diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
| commit | 220afeb0eb1b0b63fccd29e254f3179cac834c12 (patch) | |
| tree | 7ff6cc51b5e09034658fe053ccff4675a964ed13 /src/extraction/verit_checker.mli | |
| parent | a827528c0435f2006560b8cb359420bbffe85881 (diff) | |
| parent | 4c348a170ea80d20f08ccd5b20e98f56b9267485 (diff) | |
| download | smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.tar.gz smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.zip | |
Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13
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 4491410..7b8b882 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 |