Minor changes to parser files from code review.

3 files changed, 9 insertions, 9 deletions

diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index 3d9a84f06..70f60a0bc 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -14,7 +14,7 @@ class AntlrSmtLexer extends Lexer;
 options {
   exportVocab = SmtVocabulary;  // Name of the shared token vocabulary
   testLiterals = false;         // Do not check for literals by default
-  defaultErrorHandler = false;  // Skip the defaul error handling, just break with exceptions
+  defaultErrorHandler = false;  // Skip the default error handling, just break with exceptions
   k = 2;  
 }
  
@@ -130,7 +130,7 @@ WHITESPACE options { paraphrase = "whitespace"; }
   ;
 
 /**
- * Mathces and skips the newline symbols in the input.
+ * Matches and skips the newline symbols in the input.
  */
 NEWLINE options { paraphrase = "a newline"; }  
   :   ('\r' '\n' | '\r' | '\n')       { $setType(antlr::Token::SKIP); newline(); }
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index b1bb35e6f..6e0051821 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -50,7 +50,7 @@ annotation
   ;
   
 /**
- * Matches a predicate symbol from the input. 
+ * Matches a predicate symbol. 
  */
 pred_symb returns [std::string p]
   :  id:IDENTIFIER { p = id->getText(); }
@@ -58,7 +58,7 @@ pred_symb returns [std::string p]
   
 
 /**
- * Matches a propositional atom from the input. 
+ * Matches a propositional atom. 
  */
 prop_atom returns [CVC4::Expr atom]
 {
@@ -73,17 +73,18 @@ prop_atom returns [CVC4::Expr atom]
    ;
     
 /**
- * Matches an annotated proposition atom which is either a propositional atom, 
+ * Matches an annotated proposition atom, which is either a propositional atom 
  * or built of other atoms using a predicate symbol. Annotation can be added if
  * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
- * here in order to get rid of the ugly antlr non-determinism warrnings. 
+ * here in order to get rid of the ugly antlr non-determinism warnings. 
  */
+ // [chris 12/15/2009] FIXME: Where is the annotation? 
 an_atom returns [CVC4::Expr atom] 
   : atom = prop_atom  
   ;
   
 /**
- * Matches on of the unary Boolean conectives.  
+ * Matches on of the unary Boolean connectives.  
  */
 bool_connective returns [CVC4::Kind kind]
   : NOT      { kind = CVC4::NOT;     } 
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
index a68f0e783..6927888cf 100644
--- a/src/parser/smt/smt_parser.h
+++ b/src/parser/smt/smt_parser.h
@@ -31,8 +31,7 @@ class CVC4_PUBLIC SmtParser : public Parser {
 public:
 
   /**
-   * Construct the parser that uses the given expression manager and parses
-   * from the given input stream.
+   * Construct the parser that uses the given expression manager and input stream.
    * @param em the expression manager to use
    * @param input the input stream to parse
    * @param file_name the name of the file (for diagnostic output)