diff options
Diffstat (limited to 'src/trace/smtCommands.mli')
| -rw-r--r-- | src/trace/smtCommands.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index d6fa756..3cac245 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -32,21 +32,21 @@ val parse_certif : Names.identifier -> Names.identifier -> Names.identifier -> - SmtAtom.Btype.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 list * int * SmtAtom.Form.t SmtCertif.clause -> unit val interp_roots : SmtAtom.Form.t list -> Term.constr val theorem : Names.identifier -> - SmtAtom.Btype.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 list * int * SmtAtom.Form.t SmtCertif.clause -> unit val checker : - SmtAtom.Btype.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 list * int * SmtAtom.Form.t SmtCertif.clause -> unit val build_body : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> @@ -55,7 +55,7 @@ val build_body : int * SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr * (Names.identifier * Term.types) list val build_body_eq : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> @@ -71,22 +71,22 @@ val make_proof : SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) -> 'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c val core_tactic : - (SmtAtom.Btype.reify_tbl -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> int * SmtAtom.Form.t SmtCertif.clause) -> - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic val tactic : - (SmtAtom.Btype.reify_tbl -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> int * SmtAtom.Form.t SmtCertif.clause) -> - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic |