aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction/smtcoq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/extraction/smtcoq.mli')
-rw-r--r--src/extraction/smtcoq.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/extraction/smtcoq.mli b/src/extraction/smtcoq.mli
new file mode 100644
index 0000000..7b33e0f
--- /dev/null
+++ b/src/extraction/smtcoq.mli
@@ -0,0 +1,5 @@
+type solver = Zchaff | Verit
+val usage : string
+val string_of_solver : solver -> string
+val verifier_of_solver : solver -> string -> string -> bool
+val run : solver -> string -> string -> unit