diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-06 18:34:44 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-06 18:34:44 +0100 |
| commit | 00bf195620810ff5721a840f0a99417f092f5eee (patch) | |
| tree | 53eef376e9fff66b1f2ec2d13ce3bcd3a79b635c /src | |
| parent | 48e123caddd6a4c4edd60d8f39b78a5421418f40 (diff) | |
| download | smtcoq-00bf195620810ff5721a840f0a99417f092f5eee.tar.gz smtcoq-00bf195620810ff5721a840f0a99417f092f5eee.zip | |
Update extraction (only ml)
Diffstat (limited to 'src')
| -rw-r--r-- | src/extraction/Makefile | 2 | ||||
| -rw-r--r-- | src/extraction/verit_checker.ml | 3 | ||||
| -rw-r--r-- | src/extraction/zchaff_checker.ml | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 8919438..043afa1 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 ../lia -I ../euf -I ../cnf +SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../versions/native/ 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.ml b/src/extraction/verit_checker.ml index 20040bc..3f9a701 100644 --- a/src/extraction/verit_checker.ml +++ b/src/extraction/verit_checker.ml @@ -16,6 +16,7 @@ open SmtMisc open SmtCertif +open SmtCommands open SmtForm open SmtAtom open SmtTrace @@ -25,7 +26,7 @@ open Smtlib2_genConstr (* open Smt_checker *) -module Mc = Micromega +module Mc = Structures.Micromega_plugin_Certificate.Mc let mkInt = ExtrNative.of_int diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml index 60d0a38..eb28fe8 100644 --- a/src/extraction/zchaff_checker.ml +++ b/src/extraction/zchaff_checker.ml @@ -54,7 +54,7 @@ let to_coq to_lit (cstep, cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, cImmBuildProj,cImmBuildDef,cImmBuildDef2, cEqTr, cEqCgr, cEqCgrP, - cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl = + cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, cHole) confl = let step_to_coq c = match c.kind with | Res res -> |