summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager.i
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager.i')
-rw-r--r--src/expr/expr_manager.i2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 11c1e284d..f8bb55523 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -65,7 +65,7 @@
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback