diff options
Diffstat (limited to 'src/extraction/verit_checker.mli')
| -rw-r--r-- | src/extraction/verit_checker.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli index b24532e..6247001 100644 --- a/src/extraction/verit_checker.mli +++ b/src/extraction/verit_checker.mli @@ -10,7 +10,7 @@ (**************************************************************************) -module Mc = Structures.Micromega_plugin_Certificate.Mc +module Mc = CoqInterface.Micromega_plugin_Certificate.Mc val mkInt : int -> ExtrNative.uint val mkArray : 'a array -> 'a ExtrNative.parray val dump_nat : Mc.nat -> Smt_checker.nat @@ -25,7 +25,7 @@ val to_coq : 'a SmtCertif.clause -> Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray * 'a SmtCertif.clause -val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type +val btype_to_coq : SmtBtype.btype -> Smt_checker.Typ.coq_type val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop @@ -42,7 +42,7 @@ val form_interp_tbl : SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray val count_btype : int ref val count_op : int ref -val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype +val declare_sort : Smtlib2_ast.symbol -> SmtBtype.btype val declare_fun : Smtlib2_ast.symbol -> Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op |