summaryrefslogtreecommitdiff
path: root/src/theory/builtin
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/builtin')
-rw-r--r--src/theory/builtin/proof_checker.h2
-rw-r--r--src/theory/builtin/theory_builtin.h2
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.h2
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/builtin/type_enumerator.h2
5 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 8aedda650..38eea31c5 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -13,7 +13,7 @@
* Equality proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 01946b584..27492cb53 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -13,7 +13,7 @@
* Built-in theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 7f4d4ade3..7d5cde3c2 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -16,7 +16,7 @@
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 1c067f048..87ba12ed1 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -13,7 +13,7 @@
* Type rules for the builtin theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 9bfea2760..980792f94 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -13,7 +13,7 @@
* Enumerator for uninterpreted sorts and functions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
#define CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback