diff options
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Makefile | 2 | ||||
| -rw-r--r-- | src/extraction/verit_checker.mli | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 73b0ae4..354dd53 100644 --- a/src/extraction/Makefile +++ b/src/extraction/Makefile @@ -15,7 +15,7 @@ COQTOP=$(COQBIN)../ FLAGS=-rectypes COMPILEFLAGS=-cclib -lunix -SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../versions/native/ +SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../../3rdparty/alt-ergo COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa 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 |