** Don't fear the files-changed list, almost all changes are in the **

** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.

28 files changed, 184 insertions, 86 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 9d75dd31f..fdaa83b04 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** input.cpp
+/*! \file antlr_input.cpp
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A super-class for ANTLR-generated input language parsers.
  **
  ** A super-class for ANTLR-generated input language parsers
  **/
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 642dc9654..d2d885ce0 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** input.h
+/*! \file antlr_input.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Base for ANTLR parser classes.
  **
  ** Base for ANTLR parser classes.
  **/
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index d25d7b66b..b647842fa 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file antlr_input_imports.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** rief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 /*
  * The functions in this file are based on implementations in libantlr3c,
  * with only minor CVC4-specific changes.
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 53b56dcdd..adc0505db 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** bounded_token_buffer.h
+/*! \file bounded_token_buffer.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An ANTLR3 bounded token stream implementation. 
  **
  ** An ANTLR3 bounded token stream implementation. 
  ** This code is largely based on the original token buffer implementation
diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index 663e5b403..9634f016b 100644
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** bounded_token_buffer.h
+/*! \file bounded_token_buffer.h
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An ANTLR3 bounded token stream.
  **
  ** An ANTLR3 bounded token stream. The stream has a bounded
  ** lookahead/behind k. Calling LT(i) with i > k or i < -k will raise
diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp
index c9f9b66e7..5f42f0f29 100644
--- a/src/parser/bounded_token_factory.cpp
+++ b/src/parser/bounded_token_factory.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** bounded_token_factory.cpp
+/*! \file bounded_token_factory.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An ANTLR3 bounded token factory implementation.
  **
  ** An ANTLR3 bounded token factory implementation.
  **/
diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h
index faf289ef4..4d510c9e3 100644
--- a/src/parser/bounded_token_factory.h
+++ b/src/parser/bounded_token_factory.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** bounded_token_factory.h
+/*! \file bounded_token_factory.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An ANTLR3 bounded token factory.
  **
  ** An ANTLR3 bounded token factory. The factory has a fixed number of
  ** tokens that are re-used as parsing proceeds. Only use this factory
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index a53604efa..0f44e692a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1,14 +1,17 @@
 /* *******************                                                        */
-/*  Cvc.g
+/*! \file Cvc.g
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Parser for CVC-LIB input language.
  **
  ** Parser for CVC-LIB input language.
  **/
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 4a8551a7a..2b99f9a87 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** cvc_input.cpp
+/*! \file cvc_input.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 82c31813b..64c6beea7 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** cvc_input.h
+/*! \file cvc_input.h
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index a900765b5..2c4671b93 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** input.cpp
- ** Original author: cconway
- ** Major contributors: none
+/*! \file input.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A super-class for input language parsers.
  **
  ** A super-class for input language parsers
  **/
diff --git a/src/parser/input.h b/src/parser/input.h
index 926ebe156..ceec1c8bd 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** input.h
+/*! \file input.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Base for parser inputs.
  **
  ** Base for parser inputs.
  **/
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index a87ba9cf8..7748a1cca 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** memory_mapped_input_buffer.cpp
+/*! \file memory_mapped_input_buffer.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h
index c63ec5407..18618a090 100644
--- a/src/parser/memory_mapped_input_buffer.h
+++ b/src/parser/memory_mapped_input_buffer.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** memory_mapped_input_buffer.h
+/*! \file memory_mapped_input_buffer.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief ANTLR input buffer from a memory-mapped file.
  **
  ** ANTLR input buffer from a memory-mapped file.
  **/
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 286867e84..2bad12e2c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** parser.cpp
- ** Original author: cconway
- ** Major contributors: dejan, mdeters
+/*! \file parser.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Parser state implementation.
  **
  ** Parser state implementation.
  **/
diff --git a/src/parser/parser.h b/src/parser/parser.h
index e6e5a2250..3e10f632f 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** parser.h
+/*! \file parser.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A collection of state for use by parser implementations.
  **
  ** A collection of state for use by parser implementations.
  **/
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 4e4b0309f..3b62cbc57 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** parser_builder.cpp
+/*! \file parser_builder.cpp
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A builder for parsers.
  **
  ** A builder for parsers.
  **/
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 92b44a82d..ed1ab807b 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** parser_builder.h
+/*! \file parser_builder.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A builder for parsers.
  **
  ** A builder for parsers.
  **/
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index dfca01ce2..2ae38622d 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** parser_exception.h
+/*! \file parser_exception.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Exception class for parse errors.
  **
  ** Exception class for parse errors.
  **/
diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h
index 51d28e51d..85994c52c 100644
--- a/src/parser/parser_options.h
+++ b/src/parser/parser_options.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** parser_options.h
+/*! \file parser_options.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index c11f350a6..4247dba7a 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -1,14 +1,17 @@
 /* *******************                                                        */
-/*  Smt.g
+/*! \file Smt.g
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Parser for SMT-LIB input language.
  **
  ** Parser for SMT-LIB input language.
  **/
@@ -60,7 +63,6 @@ namespace CVC4 {
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -171,7 +173,7 @@ annotatedFormula[CVC4::Expr& expr]
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
-      } else if( CVC4::kind::metakind::isAssociative(kind) && 
+      } else if( CVC4::kind::isAssociative(kind) && 
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index 7c8bf19dd..c19eca080 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** smt_input.cpp
+/*! \file smt_input.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index 1d3f87668..42581ec1c 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** smt_input.h
+/*! \file smt_input.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 11ce111a6..37612901e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1,14 +1,17 @@
 /* *******************                                                        */
-/*  Smt2.g
+/*! \file Smt2.g
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): mdeters, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Parser for SMT-LIB v2 input language.
  **
  ** Parser for SMT-LIB v2 input language.
  **/
@@ -74,7 +77,6 @@ namespace CVC4 {
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -210,7 +212,7 @@ term[CVC4::Expr& expr]
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
-	 } else if( CVC4::kind::metakind::isAssociative(kind) && 
+	 } else if( CVC4::kind::isAssociative(kind) && 
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 5cf902260..2776bff7e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** smt2.h
+/*! \file smt2.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors:
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Definitions of SMT2 constants.
  **
  ** Definitions of SMT2 constants.
  **/
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 0e057db68..b54fe82e9 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** smt2.h
+/*! \file smt2.h
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors:
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Definitions of SMT2 constants.
  **
  ** Definitions of SMT2 constants.
  **/
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 5150ba010..829d6a5f8 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** smt2_input.cpp
+/*! \file smt2_input.cpp
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 962e2a987..1fa8cff1c 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** smt2_input.h
+/*! \file smt2_input.h
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
  **
  ** [[ Add file-specific comments here ]]
  **/