4 files changed, 21 insertions, 31 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 4cb4d577b..d2ac81167 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -74,6 +74,8 @@ using namespace CVC4::parser;
 #define EXPR_MANAGER ANTLR_INPUT->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_CONST
+#define MK_CONST EXPR_MANAGER->mkConst
 }
 
 /**
@@ -105,7 +107,7 @@ command returns [CVC4::Command* cmd = 0]
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
-  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_EXPR(CVC4::kind::TRUE)); }
+  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); }
   | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
   | POP_TOK SEMICOLON { cmd = new PopCommand(); }
   | declaration[cmd]
@@ -369,8 +371,8 @@ term[CVC4::Expr& f]
     LPAREN formula[f] RPAREN
 
     /* constants */
-  | TRUE_TOK  { f = MK_EXPR(CVC4::kind::TRUE); }
-  | FALSE_TOK { f = MK_EXPR(CVC4::kind::FALSE); }
+  | TRUE_TOK  { f = MK_CONST(true); }
+  | FALSE_TOK { f = MK_CONST(false); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index f02c9345c..ade8d83e7 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -2,8 +2,10 @@ AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -fvisibility=hidden
+
 # Compile generated C files using C++ compiler
 CC=$(CXX)
+AM_CFLAGS = $(AM_CXXFLAGS)
 
 noinst_LTLIBRARIES = libparsercvc.la
 
@@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF)
 dist-hook: $(ANTLR_STUFF)
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-rmdir @srcdir@/generated
-	-rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir @srcdir@/generated
+	-$(AM_V_at)rm -f @srcdir@/stamp-generated
 
 @srcdir@/stamp-generated:
-	mkdir -p @srcdir@/generated
-	touch @srcdir@/stamp-generated
+	$(AM_V_at)mkdir -p @srcdir@/generated
+	$(AM_V_at)touch @srcdir@/stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
 @srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated
-	-rm -f $(ANTLR_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g"
+	-$(AM_V_at)rm -f $(ANTLR_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g"
 
 # These don't actually depend on CvcLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 1f1a602c5..241ce62f3 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -1,10 +1,3 @@
-/*
- * cvc_parser.cpp
- *
- *  Created on: Mar 5, 2010
- *      Author: chris
- */
-
 #include <antlr3.h>
 
 #include "expr/expr_manager.h"
@@ -69,6 +62,5 @@ pANTLR3_LEXER CvcInput::getLexer() {
 }
 */
 
-} // namespace parser
-
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index a6117b4a9..9908a25aa 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -1,12 +1,7 @@
-/*
- * cvc_parser.h
- *
- *  Created on: Mar 5, 2010
- *      Author: chris
- */
+#include "cvc4parser_public.h"
 
-#ifndef CVC_PARSER_H_
-#define CVC_PARSER_H_
+#ifndef __CVC4__PARSER__CVC_INPUT_H
+#define __CVC4__PARSER__CVC_INPUT_H
 
 #include "parser/antlr_input.h"
 #include "parser/cvc/generated/CvcLexer.h"
@@ -76,8 +71,7 @@ private:
 
 }; // class CvcInput
 
-} // namespace parser
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-} // namespace CVC4
-
-#endif /* CVC_PARSER_H_ */
+#endif /* __CVC4__PARSER__CVC_INPUT_H */