aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/verit.mli
diff options
context:
space:
mode:
authorQuentin Garchery <garchery.quentin@gmail.com>2018-10-28 00:30:23 +0200
committerValentin Blot <24938579+vblot@users.noreply.github.com>2018-10-28 00:30:23 +0200
commit7940ef63c654be26b41ce20162207f3c67d0b10a (patch)
tree89d7e2a04b93a0cb37642416535637ddb45eba8b /src/verit/verit.mli
parentcefda895d15a3f7eb7bf75402beb6fae22162585 (diff)
downloadsmtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.tar.gz
smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.zip
New files SmtBtype.ml(i) for module formerly in SmtAtom
Diffstat (limited to 'src/verit/verit.mli')
-rw-r--r--src/verit/verit.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 126a02b..68ee317 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -7,7 +7,7 @@ val clear_all : unit -> unit
val import_all :
string ->
string ->
- 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
val parse_certif :
@@ -21,10 +21,10 @@ val theorem : Names.identifier -> string -> string -> unit
val checker : string -> string -> unit
val export :
out_channel ->
- SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+ SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
SmtAtom.Form.t -> unit
val call_verit :
- SmtAtom.Btype.reify_tbl ->
+ SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Form.t ->
SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->