* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

9 files changed, 13 insertions, 10 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5e7aebbec..804d3af9a 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_manager_template.cpp
+/*! \file expr_manager.cpp
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 158f17c14..8e0f23c6a 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_manager_template.h
+/*! \file expr_manager.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -210,7 +210,7 @@ public:
    *
    * @param kind the kind of expression to build
    * @param child1 the first subexpression
-   * @param children the remaining subexpressions
+   * @param otherChildren the remaining subexpressions
    * @return the n-ary expression
    */
   Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 365dc050f..a6f9f2cf6 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_template.cpp
+/*! \file expr.cpp
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 395bdff3a..c50e85ac2 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_template.h
+/*! \file expr.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -403,6 +403,7 @@ public:
    * @param types set to true to ascribe types to the output
    * expressions (might break language compliance, but good for
    * debugging expressions)
+   * @param dag the dagification threshold to use (0 == off)
    * @param language the language in which to output
    */
   void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
@@ -960,7 +961,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 964 "${template}"
+#line 965 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 1acbed978..fc7d838a1 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file kind_template.h
+/*! \file kind.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index a954a7f70..dbaba664c 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file metakind_template.h
+/*! \file metakind.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index ee04b17fd..3f24d10f8 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -118,6 +118,8 @@ public:
    * @param name an identifier
    * @param params the parameters to the type
    * @param t the type to bind to <code>name</code>
+   * @param levelZero true to bind it globally (default is to bind it
+   * locally within the current scope)
    */
   void bindType(const std::string& name,
                 const std::vector<Type>& params,
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 9359a6ab8..d559477f1 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_checker_template.cpp
+/*! \file type_checker.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 1e983e86c..ee7a93144 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_properties_template.h
+/*! \file type_properties.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none