2 files changed, 13 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 21e01e7ed..08fba893e 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -463,6 +463,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @lexer::includes {
 
+// This should come immediately after #include <antlr3.h> in the generated
+// files. See the documentation in "parser/antlr_undefines.h" for more details.
+#include "parser/antlr_undefines.h"
+
 /** This suppresses warnings about the redefinition of token symbols between different
   * parsers. The redefinitions should be harmless as long as no client: (a) #include's
   * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
@@ -487,6 +491,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @parser::includes {
 
+// This should come immediately after #include <antlr3.h> in the generated
+// files. See the documentation in "parser/antlr_undefines.h" for more details.
+#include "parser/antlr_undefines.h"
+
 #include <stdint.h>
 #include <cassert>
 #include "options/set_language.h"
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 69920403f..2370109ef 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -14,12 +14,16 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+// These headers should be the first two included.
+// See the documentation in "parser/antlr_undefines.h" for more details.
 #include <antlr3.h>
+#include "parser/antlr_undefines.h"
+
+#include "parser/cvc/cvc_input.h"
 
 #include "expr/expr_manager.h"
 #include "parser/antlr_input.h"
 #include "parser/parser_exception.h"
-#include "parser/cvc/cvc_input.h"
 #include "parser/cvc/CvcLexer.h"
 #include "parser/cvc/CvcParser.h"