4 files changed, 6 insertions, 6 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index b60876967..eadbb73a2 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -28,7 +28,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 31 "${template}"
+#line 32 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b5e4a62f0..fba1a919c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -96,7 +96,7 @@ public:
    * @param options the earlyTypeChecking field is used to configure
    * whether to do at Expr creation time.
    */
-  explicit ExprManager(const Options&);
+  explicit ExprManager(const Options& options);
 
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h
index 77cadf0ea..ea9c8371f 100644
--- a/src/include/cvc4_private.h
+++ b/src/include/cvc4_private.h
@@ -11,10 +11,10 @@
  ** 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
+ ** \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
+ ** #-inclusion of this file marks a header as private and generates a
  ** warning when the file is included improperly.
  **/
 
diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h
index cb6e486d8..cfd4405e6 100644
--- a/src/include/cvc4parser_private.h
+++ b/src/include/cvc4parser_private.h
@@ -11,10 +11,10 @@
  ** 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
+ ** \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
+ ** #-inclusion of this file marks a header as private and generates a
  ** warning when the file is included improperly.
  **/