now compiles with standard coq (including 8.6.1 from opam)

4 files changed, 108 insertions, 11 deletions

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