diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:15:25 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:15:25 +0200 |
commit | be486d634803e7bdfd455e58dbe3ed0968798eda (patch) | |
tree | 8bba73ba41522a4fb288dc7243bd3954932b7366 /src/extraction/verit_checker.mli | |
parent | a3a63ab0bceb12f03bac91ef7461061f1cb20af1 (diff) | |
parent | b40fefbb52afbc7deaa0b591d155bf2e84d0afba (diff) | |
download | smtcoq-be486d634803e7bdfd455e58dbe3ed0968798eda.tar.gz smtcoq-be486d634803e7bdfd455e58dbe3ed0968798eda.zip |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11
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 |