now compiles with standard coq (including 8.6.1 from opam)

11 files changed, 206 insertions, 17 deletions

diff --git a/.gitignore b/.gitignore
index c6a297a..9db2580 100644
--- a/.gitignore
+++ b/.gitignore
@@ -255,3 +255,90 @@ src/zchaff/zchaffParser.cmx
 src/zchaff/zchaffParser.ml.d
 src/zchaff/zchaffParser.mli.d
 src/zchaff/zchaffParser.o
+src/.Misc.aux
+src/.SMTCoq.aux
+src/.SMT_terms.aux
+src/.State.aux
+src/.Trace.aux
+src/.lia.cache
+src/cnf/.Cnf.aux
+src/euf/.Euf.aux
+src/g_smtcoq.cmi
+src/g_smtcoq.cmo
+src/g_smtcoq.cmx
+src/g_smtcoq.ml4
+src/g_smtcoq.ml4.d
+src/g_smtcoq.o
+src/lia/.Lia.aux
+src/lia/lia.cmo
+src/smtcoq_plugin.mlpack
+src/smtcoq_plugin.mlpack.d
+src/smtlib2/smtlib2_ast.cmo
+src/smtlib2/smtlib2_genConstr.cmo
+src/smtlib2/smtlib2_lex.cmo
+src/smtlib2/smtlib2_parse.cmo
+src/smtlib2/smtlib2_parse.mli
+src/smtlib2/smtlib2_util.cmo
+src/spl/.Arithmetic.aux
+src/spl/.Assumptions.aux
+src/spl/.Operators.aux
+src/spl/.Syntactic.aux
+src/trace/coqTerms.cmo
+src/trace/satAtom.cmo
+src/trace/smtAtom.cmo
+src/trace/smtCertif.cmo
+src/trace/smtCnf.cmo
+src/trace/smtCommands.cmo
+src/trace/smtForm.cmo
+src/trace/smtMisc.cmo
+src/trace/smtTrace.cmo
+src/verit/verit.cmo
+src/verit/veritLexer.cmo
+src/verit/veritParser.cmo
+src/verit/veritParser.mli
+src/verit/veritSyntax.cmo
+src/versions/standard/.Structures.aux
+src/versions/standard/Array/.PArray.aux
+src/versions/standard/Array/PArray.glob
+src/versions/standard/Array/PArray.v
+src/versions/standard/Array/PArray.v.d
+src/versions/standard/Array/PArray.vo
+src/versions/standard/Int63/.Int63.aux
+src/versions/standard/Int63/.Int63Axioms.aux
+src/versions/standard/Int63/.Int63Native.aux
+src/versions/standard/Int63/.Int63Op.aux
+src/versions/standard/Int63/.Int63Properties.aux
+src/versions/standard/Int63/Int63.glob
+src/versions/standard/Int63/Int63.v
+src/versions/standard/Int63/Int63.v.d
+src/versions/standard/Int63/Int63.vo
+src/versions/standard/Int63/Int63Axioms.glob
+src/versions/standard/Int63/Int63Axioms.v
+src/versions/standard/Int63/Int63Axioms.v.d
+src/versions/standard/Int63/Int63Axioms.vo
+src/versions/standard/Int63/Int63Native.glob
+src/versions/standard/Int63/Int63Native.v
+src/versions/standard/Int63/Int63Native.v.d
+src/versions/standard/Int63/Int63Native.vo
+src/versions/standard/Int63/Int63Op.glob
+src/versions/standard/Int63/Int63Op.v
+src/versions/standard/Int63/Int63Op.v.d
+src/versions/standard/Int63/Int63Op.vo
+src/versions/standard/Int63/Int63Properties.glob
+src/versions/standard/Int63/Int63Properties.v
+src/versions/standard/Int63/Int63Properties.v.d
+src/versions/standard/Int63/Int63Properties.vo
+src/versions/standard/Structures.glob
+src/versions/standard/Structures.v
+src/versions/standard/Structures.v.d
+src/versions/standard/Structures.vo
+src/versions/standard/structures.cmi
+src/versions/standard/structures.cmo
+src/versions/standard/structures.cmx
+src/versions/standard/structures.ml.d
+src/versions/standard/structures.mli.d
+src/versions/standard/structures.o
+src/zchaff/cnfParser.cmo
+src/zchaff/satParser.cmo
+src/zchaff/zchaff.cmo
+src/zchaff/zchaffParser.cmo
diff --git a/src/lia/lia.mli b/src/lia/lia.mli
index bb5587f..3c8e582 100644
--- a/src/lia/lia.mli
+++ b/src/lia/lia.mli
@@ -56,4 +56,4 @@ val build_lia_certif :
   my_tbl *
   Structures.Micromega_plugin_Micromega.z
   Structures.Micromega_plugin_Coq_micromega.formula *
-  Certificate.Mc.zArithProof list option
+  Structures.Micromega_plugin_Certificate.Mc.zArithProof list option
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index b90e3ff..d6fa756 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -80,7 +80,7 @@ val core_tactic :
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
-  Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic
+  Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
 val tactic :
   (SmtAtom.Btype.reify_tbl ->
    SmtAtom.Op.reify_tbl ->
@@ -89,4 +89,4 @@ val tactic :
    int * SmtAtom.Form.t SmtCertif.clause) ->
   SmtAtom.Btype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
-  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 2ec830c..3741339 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -28,4 +28,4 @@ val call_verit :
   SmtAtom.Form.t ->
   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
   int * SmtAtom.Form.t SmtCertif.clause
-val tactic : unit -> Proof_type.tactic
+val tactic : unit -> Structures.tactic
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 589e772..42e5792 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -130,3 +130,7 @@ module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
+
+
+(* Type of coq tactics *)
+type tactic = Proof_type.tactic
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index 057625c..ba095c8 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -38,3 +38,4 @@ module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
+type tactic = Proof_type.tactic
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 1cfad12..8defd9b 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -32,7 +32,7 @@
 -I versions/standard/Int63
 -I versions/standard/Array
 
--I $(COQBIN)../plugins/micromega
+-I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
 
 -extra "test" "" "cd ../unit-tests; make" ""
 -extra "ztest" "" "cd ../unit-tests; make zchaff"
@@ -54,43 +54,62 @@ versions/standard/Array/PArray.v
 
 versions/standard/Structures.v
 versions/standard/structures.ml
+versions/standard/structures.mli
 
 trace/coqTerms.ml
+trace/coqTerms.mli
 trace/satAtom.ml
+trace/satAtom.mli
 trace/smtAtom.ml
 trace/smtAtom.mli
 trace/smtCertif.ml
+trace/smtCertif.mli
 trace/smtCnf.ml
+trace/smtCnf.mli
 trace/smtCommands.ml
+trace/smtCommands.mli
 trace/smtForm.ml
 trace/smtForm.mli
 trace/smtMisc.ml
+trace/smtMisc.mli
 trace/smtTrace.ml
+trace/smtTrace.mli
 
 smtlib2/smtlib2_parse.ml
 smtlib2/smtlib2_parse.mli
+smtlib2/smtlib2_lex.ml
+smtlib2/smtlib2_lex.mli
 smtlib2/smtlib2_ast.ml
+smtlib2/smtlib2_ast.mli
 smtlib2/smtlib2_genConstr.ml
-smtlib2/smtlib2_lex.ml
+smtlib2/smtlib2_genConstr.mli
 smtlib2/smtlib2_util.ml
+smtlib2/smtlib2_util.mli
 
 verit/veritParser.ml
 verit/veritParser.mli
-verit/verit.ml
 verit/veritLexer.ml
+verit/veritLexer.mli
+verit/verit.ml
+verit/verit.mli
 verit/veritSyntax.ml
 verit/veritSyntax.mli
 
 zchaff/cnfParser.ml
+zchaff/cnfParser.mli
 zchaff/satParser.ml
+zchaff/satParser.mli
 zchaff/zchaff.ml
+zchaff/zchaff.mli
 zchaff/zchaffParser.ml
+zchaff/zchaffParser.mli
 
 cnf/Cnf.v
 
 euf/Euf.v
 
 lia/lia.ml
+lia/lia.mli
 lia/Lia.v
 
 spl/Assumptions.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index a90104c..84c10d9 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -65,7 +65,7 @@ OCAMLLIBS?=-I "."\
   -I "versions/standard"\
   -I "versions/standard/Int63"\
   -I "versions/standard/Array"\
-  -I "$(COQBIN)../plugins/micromega"
+  -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
 COQLIBS?=\
   -R "." SMTCoq\
   -I "."\
@@ -79,7 +79,7 @@ COQLIBS?=\
   -I "versions/standard"\
   -I "versions/standard/Int63"\
   -I "versions/standard/Array"\
-  -I "$(COQBIN)../plugins/micromega"
+  -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
 COQCHKLIBS?=\
   -R "." SMTCoq
 COQDOCLIBS?=\
@@ -244,13 +244,13 @@ MLFILES:=versions/standard/structures.ml\
   trace/smtMisc.ml\
   trace/smtTrace.ml\
   smtlib2/smtlib2_parse.ml\
+  smtlib2/smtlib2_lex.ml\
   smtlib2/smtlib2_ast.ml\
   smtlib2/smtlib2_genConstr.ml\
-  smtlib2/smtlib2_lex.ml\
   smtlib2/smtlib2_util.ml\
   verit/veritParser.ml\
-  verit/verit.ml\
   verit/veritLexer.ml\
+  verit/verit.ml\
   verit/veritSyntax.ml\
   zchaff/cnfParser.ml\
   zchaff/satParser.ml\
@@ -280,11 +280,30 @@ endif
 
 .SECONDARY: $(addsuffix .d,$(MLPACKFILES))
 
-MLIFILES:=trace/smtAtom.mli\
+MLIFILES:=versions/standard/structures.mli\
+  trace/coqTerms.mli\
+  trace/satAtom.mli\
+  trace/smtAtom.mli\
+  trace/smtCertif.mli\
+  trace/smtCnf.mli\
+  trace/smtCommands.mli\
   trace/smtForm.mli\
+  trace/smtMisc.mli\
+  trace/smtTrace.mli\
   smtlib2/smtlib2_parse.mli\
+  smtlib2/smtlib2_lex.mli\
+  smtlib2/smtlib2_ast.mli\
+  smtlib2/smtlib2_genConstr.mli\
+  smtlib2/smtlib2_util.mli\
   verit/veritParser.mli\
-  verit/veritSyntax.mli
+  verit/veritLexer.mli\
+  verit/verit.mli\
+  verit/veritSyntax.mli\
+  zchaff/cnfParser.mli\
+  zchaff/satParser.mli\
+  zchaff/zchaff.mli\
+  zchaff/zchaffParser.mli\
+  lia/lia.mli
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(MLIFILES))
@@ -505,8 +524,8 @@ uninstall: uninstall_me.sh
 	@echo "S versions/standard/Int63" >> .merlin
 	@echo "B versions/standard/Array" >> .merlin
 	@echo "S versions/standard/Array" >> .merlin
-	@echo "B $(COQBIN)../plugins/micromega" >> .merlin
-	@echo "S $(COQBIN)../plugins/micromega" >> .merlin
+	@echo "B $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin
+	@echo "S $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin
 
 clean::
 	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 57838ee..ec899d8 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -164,3 +164,6 @@ module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Mutils = Micromega_plugin.Mutils
+
+(* Type of coq tactics *)
+type tactic = unit Proofview.tactic
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
new file mode 100644
index 0000000..86ceb3e
--- /dev/null
+++ b/src/versions/standard/structures.mli
@@ -0,0 +1,56 @@
+val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
+val gen_constant : string list list -> string -> Term.constr lazy_t
+val int63_modules : string list list
+val int31_module : string list list
+val cD0 : Term.constr lazy_t
+val cD1 : Term.constr lazy_t
+val cI31 : Term.constr lazy_t
+val mkInt : int -> Term.constr
+val cint : Term.constr lazy_t
+val parray_modules : string list list
+val cmake : Term.constr lazy_t
+val cset : Term.constr lazy_t
+val max_array_size : int
+val mkArray : Term.types * Term.constr array -> Term.constr
+val mkTrace :
+  ('a -> Term.constr) ->
+  ('a -> 'a) ->
+  'b ->
+  Term.constr Lazy.t ->
+  Term.constr Lazy.t ->
+  Term.constr Lazy.t ->
+  Term.constr Lazy.t ->
+  int -> Term.constr -> Term.constr -> 'a ref -> Term.constr
+type names_id_t = Names.Id.t
+val dummy_loc : Loc.t
+val mkUConst :
+  Term.constr -> Safe_typing.private_constants Entries.definition_entry
+val mkTConst :
+  Term.constr ->
+  Term.constr ->
+  Term.types -> Safe_typing.private_constants Entries.definition_entry
+val error : string -> 'a
+val coqtype : Term.types Future.computation
+val declare_new_type : Names.variable -> Term.constr
+val declare_new_variable : Names.variable -> Term.constr -> Term.constr
+val extern_constr : Term.constr -> Constrexpr.constr_expr
+val vernacentries_interp : Constrexpr.constr_expr -> unit
+val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
+val lift : int -> Constr.constr -> Constr.constr
+val tclTHEN :
+  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
+val tclTHENLAST :
+  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
+val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic
+val vm_cast_no_check : Term.constr -> unit Proofview.tactic
+val mk_tactic :
+  (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) ->
+  unit Proofview.tactic
+val set_evars_tac : Term.constr -> unit Proofview.tactic
+val ppconstr_lsimpleconstr : Ppconstr.precedence
+val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr
+module Micromega_plugin_Certificate = Micromega_plugin.Certificate
+module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
+module Micromega_plugin_Micromega = Micromega_plugin.Micromega
+module Micromega_plugin_Mutils = Micromega_plugin.Mutils
+type tactic = unit Proofview.tactic
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index ff0fe51..7fbaabd 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -84,5 +84,5 @@ val make_proof :
   Environ.env ->
   SatAtom.Form.reify ->
   SatAtom.Form.t -> int * SatAtom.Form.t SmtCertif.clause
-val core_tactic : Environ.env -> 'a -> Term.types -> Proof_type.tactic
-val tactic : unit -> Proof_type.tactic
+val core_tactic : Environ.env -> 'a -> Term.types -> Structures.tactic
+val tactic : unit -> Structures.tactic