7 files changed, 22 insertions, 15 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 712273473..eb67277a1 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -394,7 +394,7 @@ public:
 
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
-};
+};/* class ExprManager */
 
 ${mkConst_instantiations}
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 2e7e3ca3d..b2f76b39d 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -164,12 +164,17 @@ class CVC4_PUBLIC Parser {
 
 protected:
   /**
-   * Create a parser state. NOTE: The parser takes "ownership" of the given
+   * Create a parser state.
+   *
+   * @attention The parser takes "ownership" of the given
    * input and will delete it on destruction.
    *
    * @param exprManager the expression manager to use when creating expressions
    * @param input the parser input
    * @param strictMode whether to incorporate strict(er) compliance checks
+   * @param parseOnly whether we are parsing only (and therefore certain checks
+   * need not be performed, like those about unimplemented features, @see
+   * unimplementedFeature())
    */
   Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b8f8a522f..c381ba5bd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -87,7 +87,7 @@ public:
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
  * the SmtEngine class, so that smt_engine.h doesn't
- * #include "expr/node.h", which is a private CVC4 header (and can lead
+ * include "expr/node.h", which is a private CVC4 header (and can lead
  * to linking errors due to the improper inlining of non-visible symbols
  * into user code!).
  *
diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp
index 06f7bb29e..10ee9bf64 100644
--- a/src/theory/datatypes/explanation_manager.cpp
+++ b/src/theory/datatypes/explanation_manager.cpp
@@ -1,11 +1,11 @@
-#include "theory/datatypes/explanation_manager.h"
-
+#include "theory/datatypes/explanation_manager.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
+using namespace CVC4::theory::datatypes;
 
 void ProofManager::setExplanation( Node n, Node jn, unsigned r ) 
 { 
diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h
index f520f142d..2d269e801 100644
--- a/src/util/propositional_query.h
+++ b/src/util/propositional_query.h
@@ -40,22 +40,22 @@ public:
   /**
    * Returns whether a node q is propositionally satisfiable.
    *
-   * @params q Node to be checked for satisfiability.
-   * @params e A number representing the effort to use between 0 (minimum effort),
+   * @param q Node to be checked for satisfiability.
+   * @param e A number representing the effort to use between 0 (minimum effort),
    *  and 1 (maximum effort).
-   * @precondition q is a ground formula.
-   * @precondition effort is between 0 and 1.
+   * @pre q is a ground formula.
+   * @pre effort is between 0 and 1.
    */
   static Result isSatisfiable(TNode q);
 
   /**
    * Returns whether a node q is a propositional tautology.
    *
-   * @params q Node to be checked for satisfiability.
-   * @params e A number representing the effort to use between 0 (minimum effort),
+   * @param q Node to be checked for satisfiability.
+   * @param e A number representing the effort to use between 0 (minimum effort),
    *  and 1 (maximum effort).
-   * @precondition q is a ground formula.
-   * @precondition effort is between 0 and 1.
+   * @pre q is a ground formula.
+   * @pre effort is between 0 and 1.
    */
   static Result isTautology(TNode q);
 
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index 6573e9b64..1146a4429 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -18,6 +18,7 @@
  ** A breadcrumb trail is left, and a function can query the breaker
  ** to see if recursion has occurred.  For example:
  **
+ ** @code
  **   int foo(int x) {
  **     RecursionBreaker<int> breaker("foo", x);
  **     if(breaker.isRecursion()) {
@@ -33,6 +34,7 @@
  **     cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
  **     return z;
  **   }
+ ** @endcode
  **
  ** Recursion occurs after a while in this example, and the recursion
  ** is broken by the RecursionBreaker.
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index c7538bc41..951a32a63 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file transitive_closure.h
+/*! \file trans_closure.h
  ** \verbatim
  ** Original author: barrett
  ** Major contributors: none