summaryrefslogtreecommitdiff
path: root/src/expr/proof_ensure_closed.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/proof_ensure_closed.h')
-rw-r--r--src/expr/proof_ensure_closed.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 7b970a71a..c54a5dfd5 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -18,11 +18,12 @@
#define CVC4__EXPR__PROOF_ENSURE_CLOSED_H
#include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
namespace CVC4 {
+class ProofGenerator;
+class ProofNode;
+
/**
* Debug check closed on Trace c. Context ctx is string for debugging.
* This method throws an assertion failure if pg cannot provide a closed
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback