summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r--src/theory/quantifiers/term_database.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index bc8851195..f809aa5b8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -262,10 +262,6 @@ public:
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
-//for bound variables
-public:
- //get bound variables in n
- static void getBoundVars( Node n, std::vector< Node >& bvs );
//for skolem
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback