5 files changed, 3 insertions, 66 deletions
diff --git a/src/theory/quantifiers/Makefile b/src/theory/quantifiers/Makefile
deleted file mode 100644
index 8ffdfb575..000000000
--- a/src/theory/quantifiers/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/quantifiers
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
deleted file mode 100644
index be24d6c67..000000000
--- a/src/theory/quantifiers/Makefile.am
+++ /dev/null
@@ -1,62 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libquantifiers.la
-
-libquantifiers_la_SOURCES = \
-	theory_quantifiers_type_rules.h \
-	theory_quantifiers.h \
-	quantifiers_rewriter.h \
-	quantifiers_rewriter.cpp \
-	theory_quantifiers.cpp \
-	instantiation_engine.h \
-	instantiation_engine.cpp \
-	trigger.h \
-	trigger.cpp \
-	candidate_generator.h \
-	candidate_generator.cpp \
-	inst_match.h \
-	inst_match.cpp \
-	model_engine.h \
-	model_engine.cpp \
-	modes.cpp \
-	modes.h \
-	term_database.h \
-	term_database.cpp \
-	first_order_model.h \
-	first_order_model.cpp \
-	model_builder.h \
-	model_builder.cpp \
-	quantifiers_attributes.h \
-	quantifiers_attributes.cpp \
-	inst_gen.h \
-	inst_gen.cpp \
-	quant_util.h \
-	quant_util.cpp \
-	inst_match_generator.h \
-	inst_match_generator.cpp \
-	macros.h \
-	macros.cpp \
-	inst_strategy_e_matching.h \
-	inst_strategy_e_matching.cpp \
-	inst_strategy_cbqi.h \
-	inst_strategy_cbqi.cpp \
-	full_model_check.h \
-	full_model_check.cpp \
-	bounded_integers.h \
-	bounded_integers.cpp \
-	first_order_reasoning.h \
-	first_order_reasoning.cpp \
-	rewrite_engine.h \
-	rewrite_engine.cpp \
-	relevant_domain.h \
-	relevant_domain.cpp \
-	symmetry_breaking.h \
-	symmetry_breaking.cpp
-
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 05461d378..7f6855fea 100755
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -29,6 +29,7 @@
 #include "util/sort_inference.h"
 #include "context/context.h"
 #include "context/context_mm.h"
+#include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1688479f3..177d8b230 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -17,6 +17,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
+#include "expr/attribute.h"
 #include "theory/theory.h"
 
 #include <map>
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index fb599e2a0..8ebde136d 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
+#include "context/cdhashmap.h"
 #include "theory/theory.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"