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/smtTrace.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/smtTrace.mli')
| -rw-r--r-- | src/trace/smtTrace.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index 533725b..57d0d42 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -25,6 +25,10 @@ val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit val get_pos : 'a SmtCertif.clause -> int val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool +val order_roots : ('a -> int) -> 'a SmtCertif.clause -> + 'a SmtCertif.clause * 'a SmtCertif.clause list +val add_scertifs : ('a SmtCertif.clause_kind * 'a list option * 'a SmtCertif.clause) list -> + 'a SmtCertif.clause -> 'a SmtCertif.clause val select : 'a SmtCertif.clause -> unit val occur : 'a SmtCertif.clause -> unit val alloc : 'a SmtCertif.clause -> int @@ -32,16 +36,16 @@ val naive_alloc : 'a SmtCertif.clause -> int val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int val to_coq : ('a -> Term.constr) -> - ('a list list * 'a list -> 'b) -> + ('a list list * 'a list -> Term.types) -> Term.types 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 * 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 -> - 'a SmtCertif.clause -> - Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list + Term.constr Lazy.t * Term.constr Lazy.t -> 'a SmtCertif.clause -> + ('a SmtCertif.clause -> Term.constr * Term.constr) option -> + Term.constr * 'a SmtCertif.clause * (Names.identifier * Term.types) list module MakeOpt : functor (Form : SmtForm.FORM) -> sig |