diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/verit/verit.mli | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/verit/verit.mli')
| -rw-r--r-- | src/verit/verit.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli index 68ee317..95959da 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -1,8 +1,8 @@ val debug : bool val import_trace : - string -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string -> (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option -> - int * SmtAtom.Form.t SmtCertif.clause + SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause val clear_all : unit -> unit val import_all : string -> @@ -22,11 +22,13 @@ val checker : string -> string -> unit val export : out_channel -> SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> - SmtAtom.Form.t -> unit + SmtAtom.Form.t list -> unit val call_verit : SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> - SmtAtom.Form.t -> - SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option -> + SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause -val tactic : unit -> Structures.tactic +val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic |