summaryrefslogtreecommitdiff
path: root/src/expr/command.i
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/command.i')
-rw-r--r--src/expr/command.i2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/command.i b/src/expr/command.i
index a4bf5473e..09e54fec0 100644
--- a/src/expr/command.i
+++ b/src/expr/command.i
@@ -6,6 +6,8 @@
%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
+%ignore CVC4::GetProofCommand;
+
%rename(beginConst) CVC4::CommandSequence::begin() const throw();
%rename(endConst) CVC4::CommandSequence::end() const throw();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback