summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/inst_match.cpp6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 271e04968..14a84ea72 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -31,8 +31,10 @@ using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
+namespace CVC4 {
+namespace theory {
+namespace inst {
InstMatch::InstMatch() {
}
@@ -878,3 +880,5 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
}
return qe->addInstantiation( f, m ) ? 1 : 0;
}
+
+}}}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback