minor doxygen build target fixes
authorMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 06:27:12 +0000 (06:27 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 06:27:12 +0000 (06:27 +0000)
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/include/cvc4_private.h
src/include/cvc4parser_private.h

index b60876967fc4aa6b3492cd08ccea899400b8d604..eadbb73a2bf3e411e446d6e1b8edddff96d5cb51 100644 (file)
@@ -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) \
index b5e4a62f0366701da012c2265eae676bb7edf8e8..fba1a919c63de9a5e67022fe20a861a143aa8109 100644 (file)
@@ -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
index 77cadf0ea569824fd377987021cd4b04987bbe8a..ea9c8371f02c37a774669b67855ff91b12d19df5 100644 (file)
  ** 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.
  **/
 
index cb6e486d819283e698d77e1144f53958305456ab..cfd4405e6fd2cd47987344d3b0a1a7e919b7878d 100644 (file)
  ** 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.
  **/