7 files changed, 63 insertions, 4 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 2bf146661..a8dc39765 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file cnf_proof.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "cnf_proof.h"
 using namespace CVC4::prop;
 
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index c43c9fc62..c35b0dfff 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -3,6 +3,7 @@
  ** \verbatim
  ** Original author: lianah
  ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -31,5 +32,5 @@ public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
 };
 
-} /* CVC4 namespace*/ 
+} /* CVC4 namespace */
 #endif /* __CVC4__CNF_PROOF_H */
diff --git a/src/proof/proof.h b/src/proof/proof.h
index f163a4ffd..3e5b54cc7 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file sat_proof.h
+/*! \file proof.h
  ** \verbatim
  ** Original author: lianah
  ** Major contributors: none
@@ -20,7 +20,6 @@
 #define __CVC4__PROOF_H
 
 #include "util/options.h"
-//#define CVC4_PROOFS
 
 #ifdef CVC4_PROOF
 #  define PROOF(x) if(Options::current()->proof) { x; }
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d6dd7b73d..2d7432cbc 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file proof_manager.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "proof/cnf_proof.h"
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 5d8b9d271..c79d26fed 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -3,6 +3,7 @@
  ** \verbatim
  ** Original author: lianah
  ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 095251da8..57bb96513 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file sat_proof.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "proof/sat_proof.h"
 #include "prop/minisat/core/Solver.h"
 
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 4f9ba8e4a..4641ea4cc 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -190,7 +190,8 @@ public:
    * Constructs the empty clause resolution from the final conflict
    * 
    * @param conflict 
-   */void finalizeProof(::Minisat::CRef conflict);
+   */
+  void finalizeProof(::Minisat::CRef conflict);
 
   /// clause registration methods 
   ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);