Some cleanup and copyright updating

* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles

2 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
index 97c710219..d12c67f6a 100644
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ b/src/theory/rewriterules/rr_candidate_generator.h
@@ -32,7 +32,7 @@ typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
 
 //New CandidateGenerator. They have a simpler semantic than the old one
 
-// Just iterate amoung the equivalence classes
+// Just iterate among the equivalence classes
 // node::Null() must be given to reset
 class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
 private:
@@ -54,7 +54,7 @@ public:
   };
 };
 
-// Just iterate amoung the equivalence class of the given node
+// Just iterate among the equivalence class of the given node
 // node::Null() *can't* be given to reset
 class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
 private:
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 63728a95b..636a4dbc1 100644
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -180,7 +180,7 @@ public:
   /** If reset, or getNextMatch return false they remove from the
       InstMatch the binding that they have previously created */
 
-  /** virtual Matcher in order to have definned behavior */
+  /** virtual Matcher in order to have defined behavior */
   virtual ~Matcher(){};
 };
 
@@ -195,7 +195,7 @@ private:
   std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens;
   /** the variable that have been set by this matcher (during its own reset) */
   std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */
-  /** the representant of the argument of the term given by the last reset */
+  /** the representative of the argument of the term given by the last reset */
   std::vector< Node > d_reps;
 public:
   /** The pattern we are producing matches for */
@@ -250,7 +250,7 @@ public:
 PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe );
 PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe );
 
-/** return true if whatever Node is subsituted for the variables the
+/** return true if whatever Node is substituted for the variables the
     given Node can't match the pattern */
 bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars);