minor fixes for correct doxygen output

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 718fd58f49061d4962d770084d8e56e244cbf9a5..3b12327728b574c5bd54b02c0a7cf077d0cab6a7 100644 (file)
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -28,10 +28,10 @@ namespace CVC4 {
 namespace kind {
 
 enum Kind_t {
-  UNDEFINED_KIND = -1, /*! undefined */
-  NULL_EXPR, /*! Null kind */
+  UNDEFINED_KIND = -1, /**< undefined */
+  NULL_EXPR, /**< Null kind */
 ${kind_decls}
-  LAST_KIND
+  LAST_KIND /**< marks the upper-bound of this enumeration */
 
 };/* enum Kind_t */
 

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index c4604d40ebd19dc892c46bb1a2c9332eba767b8e..515b7978c900682e8ea0a7a93e695921e46cbec5 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -96,11 +96,11 @@ struct NodeValueCompare {
  * mean, see src/theory/builtin/kinds.
  */
 enum MetaKind_t {
-  INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */
-  VARIABLE, /*! special node kinds: no operator */
-  OPERATOR, /*! operators that get "inlined" */
-  PARAMETERIZED, /*! parameterized ops (like APPLYs) that carry extra data */
-  CONSTANT /*! constants */
+  INVALID = -1, /**< special node non-kinds like NULL_EXPR or LAST_KIND */
+  VARIABLE, /**< special node kinds: no operator */
+  OPERATOR, /**< operators that get "inlined" */
+  PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */
+  CONSTANT /**< constants */
 };/* enum MetaKind_t */
 
 }/* CVC4::kind::metakind namespace */

diff --git a/src/expr/mkkind b/src/expr/mkkind
index a417b787171959e27ec9b6748cc26b1794fe28f4..ab80224eb46cd6814ec4fffdff730e4816d8e6b9 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -106,7 +106,7 @@ function register_kind {
   nc=$2
   comment=$3
 
-  kind_decls="${kind_decls}  $r, /*! $comment */
+  kind_decls="${kind_decls}  $r, /**< $comment */
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index cc8c780a85b4c26843bd44cb81e61bd13b2bf3ae..3b9c419734bebbe4af8026526dd121f482caba8a 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -136,7 +136,7 @@
  ** Regarding the backing store (typically on the stack): the file
  ** below provides the template:
  **
- **   template <unsigned nchild_thresh> class NodeBuilder;
+ **   template < unsigned nchild_thresh > class NodeBuilder;
  **
  **     The default:
  **

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b35f3eafe7a4aeb60e53a24b10012cfb2468486c..9d152a9159d13791262bed97dcdcea7f397858d8 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -147,7 +147,6 @@ protected:
    * Caches the pair of the node and the literal corresponding to the
    * translation.
    * @param node the node
-   * @param lit the literal
    */
   bool hasLiteral(TNode node) const;
 

diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
index 38bc065550590e31bf5e6414cfad202f4198261c..6e442ded9d41462fd26e2fe55cb0100e6a4a12c1 100644 (file)
--- a/src/theory/arith/unate_propagator.cpp
+++ b/src/theory/arith/unate_propagator.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file arith_propagator.cpp
+/*! \file unate_propagator.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none

diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index 88020b52bd73d8c677afb0d5594ff18a754ef012..1aab795cb711f7c8cbacc1bdd5cb1b1a6ecb1b61 100644 (file)
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file arith_propagator.h
+/*! \file unate_propagator.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none

diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 4d50eb71257ea262fb6ca32ed63ea168579dbdf5..96e367e48ddfa9e1ed1220667ff1ae08db1bbc2d 100644 (file)
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -178,8 +178,8 @@ class CongruenceClosure {
   CareSet d_careSet;
 
   // === STATISTICS ===
-  AverageStat d_explanationLength;/*! average explanation length */
-  IntStat d_newSkolemVars;/*! new vars created */
+  AverageStat d_explanationLength;/**< average explanation length */
+  IntStat d_newSkolemVars;/**< new vars created */
 
   static inline bool isCongruenceOperator(Kind k) {
     return isInCongruenceOperatorList<CongruenceOperatorList>(k);