1 files changed, 16 insertions, 14 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 1e6badc98..f768f307d 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -16,6 +16,8 @@
  ** Resolution proof
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__SAT__PROOF_H
 #define __CVC4__SAT__PROOF_H
 
@@ -26,22 +28,23 @@
 #include <ext/hash_map>
 #include <ext/hash_set>
 #include <sstream>
+
 namespace Minisat {
-class Solver;
-typedef uint32_t CRef;
-}
+  class Solver;
+  typedef uint32_t CRef;
+}/* Minisat namespace */
 
 #include "prop/minisat/core/SolverTypes.h"
 #include "util/proof.h"
 
 namespace std {
-using namespace __gnu_cxx;
-}
+  using namespace __gnu_cxx;
+}/* std namespace */
 
 namespace CVC4 {
+
 /** 
  * Helper debugging functions
- * 
  */
 void printDebug(::Minisat::Lit l);
 void printDebug(::Minisat::Clause& c); 
@@ -56,7 +59,7 @@ struct ResStep {
     id(i),
     sign(s)
   {}
-};
+};/* struct ResStep */
 
 typedef std::vector< ResStep > ResSteps; 
 typedef std::set < ::Minisat::Lit> LitSet; 
@@ -76,8 +79,7 @@ public:
   ClauseId  getStart()     { return d_start; }
   ResSteps& getSteps()     { return d_steps; }
   LitSet*   getRedundant() { return d_redundantLits; }
-};
-
+};/* class ResChain */
 
 typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
 typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
@@ -98,7 +100,7 @@ private:
 public:
   ProofProxy(SatProof* pf);
   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
-};
+};/* class ProofProxy */
 
 class SatProof : public Proof {
 protected:
@@ -217,7 +219,7 @@ public:
   void     storeUnitResolution(::Minisat::Lit lit); 
   
   ProofProxy* getProxy() {return d_proxy; } 
-};
+};/* class SatProof */
 
 class LFSCSatProof: public SatProof {
 private:
@@ -251,8 +253,8 @@ public:
     d_seenInput()
   {} 
   virtual void toStream(std::ostream& out);  
-};
+};/* class LFSCSatProof */
 
-}
+}/* CVC4 namespace */
 
-#endif
+#endif /* __CVC4__SAT__PROOF_H */