5 files changed, 75 insertions, 85 deletions
diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h
index 3fde5f54b..740665f04 100644
--- a/src/include/cvc4_private.h
+++ b/src/include/cvc4_private.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file cvc4_private.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly
- **
- ** #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, Morgan Deters, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
 
 #ifndef CVC5_PRIVATE_H
 #define CVC5_PRIVATE_H
diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h
index b80086809..2062d4107 100644
--- a/src/include/cvc4_private_library.h
+++ b/src/include/cvc4_private_library.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file cvc4_private_library.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly
- **
- ** #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, Mathias Preiner, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
 
 #ifndef CVC5_PRIVATE_LIBRARY_H
 #define CVC5_PRIVATE_LIBRARY_H
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index 6e50120fd..ede5f5223 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file cvc4_public.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Macros that should be defined everywhere during the building of
- ** the libraries and driver binary, and also exported to the user.
- **
- ** Macros that should be defined everywhere during the building of
- ** the libraries and driver binary, and also exported to the user.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Macros that should be defined everywhere during the building of
+ * the libraries and driver binary, and also exported to the user.
+ */
 
 #ifndef CVC5_PUBLIC_H
 #define CVC5_PUBLIC_H
diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h
index 357dc9977..fd66ba394 100644
--- a/src/include/cvc4parser_private.h
+++ b/src/include/cvc4parser_private.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file cvc4parser_private.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly.
- **
- ** #-inclusion of this file marks a header as private and generates a
- ** warning when the file is included improperly.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
 
 #ifndef __CVC4PARSER_PRIVATE_H
 #define __CVC4PARSER_PRIVATE_H
diff --git a/src/include/cvc4parser_public.h b/src/include/cvc4parser_public.h
index d825c3b81..408183a2d 100644
--- a/src/include/cvc4parser_public.h
+++ b/src/include/cvc4parser_public.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file cvc4parser_public.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Macros that should be defined everywhere during the building of
- ** the libraries and driver binary, and also exported to the user.
- **
- ** Macros that should be defined everywhere during the building of
- ** the libraries and driver binary, and also exported to the user.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Macros that should be defined everywhere during the building of the
+ * libraries and driver binary, and also exported to the user.
+ */
 
 #ifndef __CVC4PARSER_PUBLIC_H
 #define __CVC4PARSER_PUBLIC_H