Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.

I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:

  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0

1 files changed, 22 insertions, 7 deletions

diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h
index 3c95ab126..676025d03 100644
--- a/src/context/cdmaybe.h
+++ b/src/context/cdmaybe.h
@@ -1,8 +1,23 @@
-/**
- * This implements a CDMaybe.
- * This has either been set in the context or it has not.
- * T must have a default constructor and support assignment.
- */
+/*********************                                                        */
+/*! \file cdmaybe.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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
+ **
+ ** \brief A context-dependent "maybe" template type
+ **
+ ** This implements a CDMaybe.
+ ** This has either been set in the context or it has not.
+ ** Template parameter T must have a default constructor and support
+ ** assignment.
+ **/
 
 #include "cvc4_private.h"
 
@@ -33,7 +48,7 @@ public:
     d_flag.set(true);
   }
 
-}; /* class CDRaised */
+};/* class CDRaised */
 
 template <class T>
 class CDMaybe {
@@ -58,7 +73,7 @@ public:
     Assert(isSet());
     return d_data.get().second;
   }
-}; /* class CDMaybe<T> */
+};/* class CDMaybe<T> */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */