3 files changed, 11 insertions, 9 deletions
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