From f06ae104dc3caf9b4ff01a0b2d49b09ace88faad Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 15 Feb 2013 11:19:08 -0500 Subject: Some cleanup and copyright updating * update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles --- src/theory/rewriterules/rr_inst_match.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/rewriterules/rr_inst_match.h') 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 & vars); -- cgit v1.2.3