aboutsummaryrefslogtreecommitdiffstats
path: root/src/zchaff/zchaff.mli
diff options
context:
space:
mode:
authorQuentin Garchery <garchery.quentin@gmail.com>2018-10-27 20:08:44 +0200
committerValentin Blot <24938579+vblot@users.noreply.github.com>2018-10-28 00:39:25 +0200
commitfaaa2848c37444f8f37ac432c25f9f813e1df39b (patch)
tree2672d165fd13b5262005406d1496bc6a14e8b521 /src/zchaff/zchaff.mli
parent7940ef63c654be26b41ce20162207f3c67d0b10a (diff)
downloadsmtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz
smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip
Adding support for lemmas in the command verit
Diffstat (limited to 'src/zchaff/zchaff.mli')
-rw-r--r--src/zchaff/zchaff.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index 7fbaabd..6a873ec 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -53,7 +53,7 @@ val certif_ops :
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t
+ Term.constr lazy_t * Term.constr lazy_t
val ccertif : Term.constr lazy_t
val cCertif : Term.constr lazy_t
val cchecker_b_correct : Term.constr lazy_t