5 files changed, 7 insertions, 7 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 74434f499..5aa1e53e4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -342,7 +342,7 @@ command returns [CVC4::Command* cmd = NULL]
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[expr, expr2]
     { cmd = new AssertCommand(expr); }
-  | /* checksat */
+  | /* check-sat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( term[expr, expr2]
       { if(PARSER_STATE->strictModeEnabled()) {
@@ -781,7 +781,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
           args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
-	       It just so happens expr should already by the only argument. */
+         * It just so happens expr should already be the only argument. */
         assert( expr == args[0] );
       } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2ae31e810..61e0999e9 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -189,7 +189,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       }
       */
       PARSER_STATE->includeFile(name /* , inclArgs */ );
-      // The command of the included file will be produced at the new parseCommand call
+      // The command of the included file will be produced at the next parseCommand() call
       cmd = new EmptyCommand("include::" + name);
     }
   | EOF
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 3e6aa82b7..edffaa01f 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -107,7 +107,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) {
     Debug("parser") << "Can't open " << fileName << std::endl;
     return false;
   }
-  // Samething than the predefined PUSHSTREAM(in);
+  // Same thing as the predefined PUSHSTREAM(in);
   lexer->pushCharStream(lexer,in);
   // restart it
   //lexer->rec->state->tokenStartCharIndex	= -10;
@@ -163,7 +163,7 @@ void Tptp::includeFile(std::string fileName) {
   // Test in the directory of the actual parsed file
   std::string currentDirFileName;
   if(inputName != "<stdin>") {
-    // TODO: Use dirname ot Boost::filesystem?
+    // TODO: Use dirname or Boost::filesystem?
     size_t pos = inputName.rfind('/');
     if(pos != std::string::npos) {
       currentDirFileName = std::string(inputName, 0, pos + 1);
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index eb49d7dcc..e180d1524 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -203,7 +203,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name,
 
 inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
   // For SZS ontology compliance.
-  // If we're in cnf() though, conjectures don't result in "Theorem" or
+  // if we're in cnf() though, conjectures don't result in "Theorem" or
   // "CounterSatisfiable".
   if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
     d_hasConjecture = true;
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index 19e928e7e..cb2bcd3a3 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -64,7 +64,7 @@ public:
 
   /** Get the language that this Input is reading. */
   InputLanguage getLanguage() const throw() {
-    return language::input::LANG_SMTLIB_V2;
+    return language::input::LANG_TPTP;
   }
 
 protected: