summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r--src/expr/expr_template.h11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 15938b160..349795156 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -21,18 +21,19 @@
#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H
-#include "expr/type.h"
#include <string>
#include <iostream>
#include <stdint.h>
+#include "util/exception.h"
+
${includes}
// This is a hack, but an important one: if there's an error, the
// 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 36 "${template}"
+#line 37 "${template}"
namespace CVC4 {
@@ -41,6 +42,8 @@ template <bool ref_count>
class NodeTemplate;
class Expr;
+class ExprManager;
+class Type;
namespace expr {
class CVC4_PUBLIC ExprSetDepth;
@@ -553,13 +556,13 @@ public:
static inline void setPrintTypes(std::ostream& out, bool printTypes) {
out.iword(s_iosIndex) = printTypes;
}
-};
+};/* class ExprPrintTypes */
}/* CVC4::expr namespace */
${getConst_instantiations}
-#line 388 "${template}"
+#line 566 "${template}"
namespace expr {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback