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.mli17
1 files changed, 0 insertions, 17 deletions
diff --git a/src/extraction/smtcoq.mli b/src/extraction/smtcoq.mli
deleted file mode 100644
index bf62ec3..0000000
--- a/src/extraction/smtcoq.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(**************************************************************************)
-(* *)
-(* SMTCoq *)
-(* Copyright (C) 2011 - 2022 *)
-(* *)
-(* See file "AUTHORS" for the list of authors *)
-(* *)
-(* This file is distributed under the terms of the CeCILL-C licence *)
-(* *)
-(**************************************************************************)
-
-
-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