summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r--src/expr/expr_manager_template.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8e02c8ca4..70f4f8453 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -25,7 +25,6 @@
#include "expr/kind.h"
#include "expr/type.h"
-#include "expr/expr.h"
${includes}
@@ -33,11 +32,12 @@ ${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 36 "${template}"
namespace CVC4 {
class Expr;
+class TypeCheckingException;
class SmtEngine;
class NodeManager;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback