From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 27 Oct 2018 20:08:44 +0200 Subject: Adding support for lemmas in the command verit --- src/trace/smtTrace.mli | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'src/trace/smtTrace.mli') 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 -- cgit