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/trace/smtCommands.mli | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/trace/smtCommands.mli')
| -rw-r--r-- | src/trace/smtCommands.mli | 46 |
1 files changed, 26 insertions, 20 deletions
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index 3cac245..6248270 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -7,7 +7,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 : Term.constr lazy_t @@ -53,6 +53,7 @@ val build_body : Term.constr -> Term.constr -> int * SmtAtom.Form.t SmtCertif.clause -> + (SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr) option -> Term.constr * Term.constr * (Names.identifier * Term.types) list val build_body_eq : SmtBtype.reify_tbl -> @@ -63,30 +64,35 @@ val build_body_eq : Term.constr -> Term.constr -> int * SmtAtom.Form.t SmtCertif.clause -> + (SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr) option -> Term.constr * Term.constr * (Names.identifier * Term.types) list val get_arguments : Term.constr -> Term.constr * Term.constr val make_proof : - ('a -> - 'b -> - SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) -> - 'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c -val core_tactic : - (SmtBtype.reify_tbl -> - SmtAtom.Op.reify_tbl -> - SmtAtom.Form.t -> - SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> - int * SmtAtom.Form.t SmtCertif.clause) -> - SmtBtype.reify_tbl -> - SmtAtom.Op.reify_tbl -> - SmtAtom.Atom.reify_tbl -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> + 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) -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.reify -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> + SmtAtom.Form.t -> SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause +val core_tactic : + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> + 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) -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> + Term.constr list -> Structures.constr_expr list -> Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic val tactic : - (SmtBtype.reify_tbl -> - SmtAtom.Op.reify_tbl -> - SmtAtom.Form.t -> - SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> - int * SmtAtom.Form.t SmtCertif.clause) -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> + 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) -> SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> - SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> + Term.constr list -> Structures.constr_expr list -> Structures.tactic |