From 02c793249635ca25e1d611125074e6afdd91533f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 16 Dec 2010 00:36:53 +0000
Subject: [PATCH] minor fixes for correct doxygen output

---
 src/expr/kind_template.h              |  6 +++---
 src/expr/metakind_template.h          | 10 +++++-----
 src/expr/mkkind                       |  2 +-
 src/expr/node_builder.h               |  2 +-
 src/prop/cnf_stream.h                 |  1 -
 src/theory/arith/unate_propagator.cpp |  2 +-
 src/theory/arith/unate_propagator.h   |  2 +-
 src/util/congruence_closure.h         |  4 ++--
 8 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 718fd58f4..3b1232772 100644
--- 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 c4604d40e..515b7978c 100644
--- 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 a417b7871..ab80224eb 100755
--- 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 cc8c780a8..3b9c41973 100644
--- 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 b35f3eafe..9d152a915 100644
--- 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 38bc06555..6e442ded9 100644
--- 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 88020b52b..1aab795cb 100644
--- 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 4d50eb712..96e367e48 100644
--- 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);
-- 
2.30.2