5 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index c63f8b51d..fbed7ffb5 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -16,9 +16,9 @@
 #include "theory/uf/eq_proof.h"
 
 #include "base/configuration.h"
-#include "expr/proof.h"
-#include "expr/proof_checker.h"
 #include "options/uf_options.h"
+#include "proof/proof.h"
+#include "proof/proof_checker.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h
index 55f7db3ba..caeda828e 100644
--- a/src/theory/uf/proof_checker.h
+++ b/src/theory/uf/proof_checker.h
@@ -19,8 +19,8 @@
 #define CVC5__THEORY__UF__PROOF_CHECKER_H
 
 #include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_node.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index ab36cd9df..b4522d9df 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -15,9 +15,9 @@
 
 #include "theory/uf/proof_equality_engine.h"
 
-#include "expr/lazy_proof_chain.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
+#include "proof/lazy_proof_chain.h"
+#include "proof/proof_node.h"
+#include "proof/proof_node_manager.h"
 #include "theory/rewriter.h"
 #include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine.h"
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 4ca13d93f..0c093d4b2 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -22,10 +22,10 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
-#include "expr/buffered_proof_generator.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "theory/eager_proof_generator.h"
+#include "proof/buffered_proof_generator.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/lazy_proof.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9cf47bab3..1afb8cc31 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -21,11 +21,11 @@
 #include <sstream>
 
 #include "expr/node_algorithm.h"
-#include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "proof/proof_node_manager.h"
 #include "smt/logic_exception.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"