aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/verit.mli
diff options
context:
space:
mode:
authorValentin Blot <24938579+vblot@users.noreply.github.com>2017-11-24 18:06:20 +0100
committerValentin Blot <24938579+vblot@users.noreply.github.com>2017-11-24 18:06:20 +0100
commita11eaaddc674c8dbce54c0a0c3ceb1059a0059f0 (patch)
tree4a934a82dc23b9fa8d0089dc2a95cbbe820733ca /src/verit/verit.mli
parent6566176e1f87838bada8c04ba80e608e8c7e958f (diff)
downloadsmtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.tar.gz
smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.zip
- auto-generated mli files for future documentation
- new Makefiles to handle these mli
Diffstat (limited to 'src/verit/verit.mli')
-rw-r--r--src/verit/verit.mli31
1 files changed, 31 insertions, 0 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
new file mode 100644
index 0000000..2ec830c
--- /dev/null
+++ b/src/verit/verit.mli
@@ -0,0 +1,31 @@
+val debug : bool
+val import_trace :
+ string ->
+ (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+ int * SmtAtom.Form.t SmtCertif.clause
+val clear_all : unit -> unit
+val import_all :
+ string ->
+ string ->
+ SmtAtom.Btype.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 :
+ Names.identifier ->
+ Names.identifier ->
+ Names.identifier ->
+ Names.identifier ->
+ Names.identifier ->
+ Names.identifier -> Names.identifier -> string -> string -> unit
+val theorem : Names.identifier -> string -> string -> unit
+val checker : string -> string -> unit
+val export :
+ out_channel ->
+ SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit
+val call_verit :
+ SmtAtom.Btype.reify_tbl ->
+ SmtAtom.Op.reify_tbl ->
+ SmtAtom.Form.t ->
+ SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+ int * SmtAtom.Form.t SmtCertif.clause
+val tactic : unit -> Proof_type.tactic