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, 9 insertions, 8 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 15a383d92..668b57b40 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat.cpp
+/*! \file theory_proxy.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan, taking, mdeters
- ** Minor contributors (to current version): kshitij
+ ** Major contributors: lianah, dejan, kshitij, mdeters
+ ** Minor contributors (to current version): barrett, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -80,12 +80,13 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
 
 SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   TNode n = d_theoryEngine->getNextDecisionRequest();
-  if(not n.isNull())
+  if(not n.isNull()) {
     return d_cnfStream->getLiteral(n);
-  
+  }
+
   // If theory doesn't give us a deicsion ask the decision engine. It
-  // may return in undefSatLiteral in which case the sat solver figure
-  // it out something
+  // may return in undefSatLiteral in which case the sat solver uses
+  // whatever default heuristic it has.
   Assert(d_decisionEngine != NULL);
   Assert(stopSearch != true);
   SatLiteral ret = d_decisionEngine->getNext(stopSearch);