V8.7 (#36)

Port SMTCoq to Coq-8.7

12 files changed, 1025 insertions, 647 deletions

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index c286f56..dbf3d62 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -114,6 +114,8 @@ let assert_before = Tactics.assert_tac
 
 let vm_conv = Reduction.vm_conv
 let vm_cast_no_check = Tactics.vm_cast_no_check
+let cbv_vm = Vnorm.cbv_vm
+
 let mk_tactic tac gl =
   let env = Tacmach.pf_env gl in
   let sigma = Tacmach.project gl in
@@ -128,15 +130,28 @@ let constrextern_extern_constr =
 
 let get_rel_dec_name = fun _ -> Names.Anonymous
 
+(* Eta-expanded to get rid of optional arguments *)
+let retyping_get_type_of env = Retyping.get_type_of env
+
 
-(* Old packaging of plugins *)
+(* Micromega *)
 module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
 
+let micromega_coq_proofTerm =
+  Coq_micromega.M.coq_proofTerm
+
+let micromega_dump_proof_term p =
+  Coq_micromega.dump_proof_term p
+
 
 (* Types in the Coq source code *)
 type tactic = Proof_type.tactic
 type names_id = Names.identifier
 type constr_expr = Topconstr.constr_expr
+
+(* EConstr *)
+type econstr = Term.constr
+let econstr_of_constr e = e
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index b4d9731..9ec21d2 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -24,7 +24,6 @@ val mkTrace :
   'b ->
   'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr
 type names_id_t = Names.identifier
-val dummy_loc : Pp.loc
 val mkUConst : Term.constr -> Entries.definition_entry
 val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry
 val error : string -> 'a
@@ -40,8 +39,11 @@ val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term
 val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val assert_before : Names.name -> Term.types -> Proof_type.tactic
+
 val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function
 val vm_cast_no_check : Term.constr -> Proof_type.tactic
+val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr
+
 val mk_tactic :
   (Environ.env ->
    Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) ->
@@ -50,16 +52,24 @@ val set_evars_tac : 'a -> Proof_type.tactic
 val ppconstr_lsimpleconstr : Ppconstr.precedence
 val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr
 val get_rel_dec_name : 'a -> Names.name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
 
 
-(* Old packaging of plugins *)
+(* Micromega *)
 module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
 
+val micromega_coq_proofTerm : Term.constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr
+
 
 (* Types in the Coq source code *)
 type tactic = Proof_type.tactic
 type names_id = Names.identifier
 type constr_expr = Topconstr.constr_expr
+
+(* EConstr *)
+type econstr = Term.constr
+val econstr_of_constr : Term.constr -> econstr
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index d4e45fc..9a90d39 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -11,12 +11,41 @@
 
 
 Require Import Bvector.
-Require Export BigNumPrelude.
+(* Require Export BigNumPrelude. *)
 Require Import Int31 Cyclic31.
 Require Export Int63Native.
 Require Export Int63Op.
 Require Import Psatz.
 
+Local Open Scope Z_scope.
+
+
+(* Taken from BigNumPrelude *)
+
+ Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
+ Proof.
+  intros p x Hle;destruct (Z_le_gt_dec 0 p).
+  apply  Zdiv_le_lower_bound;auto with zarith.
+  replace (2^p) with 0.
+  destruct x;compute;intro;discriminate.
+  destruct p;trivial;discriminate.
+ Qed.
+
+ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
+ Proof.
+  intros p x y H;destruct (Z_le_gt_dec 0 p).
+  apply Zdiv_lt_upper_bound;auto with zarith.
+  apply Z.lt_le_trans with y;auto with zarith.
+  rewrite <- (Z.mul_1_r y);apply Z.mul_le_mono_nonneg;auto with zarith.
+  assert (0 < 2^p);auto with zarith.
+  replace (2^p) with 0.
+  destruct x;change (0<y);auto with zarith.
+  destruct p;trivial;discriminate.
+ Qed.
+
+
+(* Int63Axioms *)
+
 Definition wB := (2^(Z_of_nat size)).
 
 Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99) : int63_scope.
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
index 85ea0c7..8f78691 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -12,7 +12,7 @@
 
 Require Import Int31 Cyclic31.
 Require Export Int63Native.
-Require Import BigNumPrelude.
+(* Require Import BigNumPrelude. *)
 Require Import Bvector.
 
 
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index cb1e1f5..9f24c54 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -16,9 +16,33 @@ Require Import Int31 Cyclic31.
 Require Export Int63Axioms.
 Require Import Eqdep_dec.
 Require Import Psatz.
+Require Import Znumtheory Zpow_facts.
 
 Local Open Scope int63_scope.
 Local Open Scope Z_scope.
+
+
+Notation Zpower_2 := Z.pow_2_r.
+Notation Zpower_Zsucc := Z.pow_succ_r.
+
+
+(* Taken from BigNumPrelude *)
+
+Lemma Zlt0_not_eq : forall n, 0<n -> n<>0.
+Proof.
+ auto with zarith.
+Qed.
+
+Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H).
+
+Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
+ Proof.
+  intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto.
+  case (Z.le_gt_cases b a); intros H4; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
+ Qed.
+
+
 (** Trivial lemmas without axiom *)
 
 Lemma wB_diff_0 : wB <> 0.
@@ -406,7 +430,18 @@ Proof.
  case_eq ((i / j < j)%int);[ | rewrite <- Bool.not_true_iff_false];
   rewrite ltb_spec, div_spec;intros.
  assert ([| j + (i / j)%int|] = [|j|] + [|i|]/[|j|]).
-   rewrite add_spec, Zmod_small;rewrite div_spec;auto with zarith.
+ {
+   rewrite add_spec, Zmod_small;rewrite div_spec; auto with zarith.
+   split.
+   - apply Z.add_nonneg_nonneg.
+     + apply Z.lt_le_incl; apply Z.le_lt_trans with (2 := H). apply Z_div_pos.
+       * apply Z.lt_gt. abstract omega.
+       * abstract omega.
+     + apply Z_div_pos.
+       * apply Z.lt_gt. assumption.
+       * abstract omega.
+   - abstract omega.
+ }
  apply Hrec;rewrite lsr_spec, H0, to_Z_1;change (2^1) with 2.
  split; [ | apply sqrt_test_false;auto with zarith].
  replace ([|j|] + [|i|]/[|j|]) with
@@ -414,9 +449,22 @@ Proof.
  rewrite Z_div_plus_full_l; auto with zarith.
  assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith).
  assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / 2) ; auto with zarith.
- case (Zle_lt_or_eq 1 [|j|]); auto with zarith; intros Hj1.
+ case (Zle_lt_or_eq 1 [|j|]); auto with zarith.
+ {
+   intro. apply Z_div_pos.
+   - apply Zgt_pos_0.
+   - apply Z.add_nonneg_nonneg.
+     + abstract omega.
+     + assumption.
+ }
+ intros Hj1.
  rewrite <- Hj1, Zdiv_1_r.
  assert (0 <= ([|i|] - 1) /2)%Z;[ |apply Z_div_pos]; auto with zarith.
+ {
+   apply Z_div_pos.
+   - apply Zgt_pos_0.
+   - abstract omega.
+ }
  apply sqrt_main;auto with zarith.
  split;[apply sqrt_test_true | ];auto with zarith.
 Qed.
@@ -562,7 +610,16 @@ Proof.
   replace [|(1 << (digits - 1))|] with (wB/2); auto.
   rewrite lsr_spec; auto.
   replace (2^[|1|]) with 2%Z; auto.
-  split; auto with zarith.
+  split.
+  {
+    apply Z.add_nonneg_nonneg.
+    - apply Z_div_pos.
+      + apply Zgt_pos_0.
+      + assumption.
+    - apply Z_div_pos.
+      + apply Zgt_pos_0.
+      + abstract omega.
+  }
   assert ([|i|]/2 < wB/2); auto with zarith.
   apply Zdiv_lt_upper_bound; auto with zarith.
  apply Hrec; rewrite H; clear u H.
@@ -574,6 +631,13 @@ Proof.
         (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])); try ring.
  rewrite Z_div_plus_full_l; auto with zarith.
  assert (0 <= ([|j|] - 2 + [||WW ih il||] / [|j|]) / 2) ; auto with zarith.
+ {
+   apply Z_div_pos.
+   - apply Zgt_pos_0.
+   - apply Z.add_nonneg_nonneg.
+     + abstract omega.
+     + assumption.
+ }
  apply sqrt_test_false; auto with zarith.
  apply sqrt_main; auto with zarith.
  contradict Hij; apply Zle_not_lt.
@@ -1091,7 +1155,8 @@ Proof.
    replace [|j|] with (d2 + [|i|])%Z.
  2: unfold d2; ring.
  rewrite Zpower_exp; auto with zarith.
- rewrite Zdiv_mult_cancel_r; auto with zarith.
+ rewrite Zdiv_mult_cancel_r.
+ 2: (apply Zlt0_not_eq; apply Z.pow_pos_nonneg; [apply Pos2Z.is_pos|assumption]).
  2: unfold d2; auto with zarith.
  rewrite (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith.
  2: apply Zlt_gt; apply Zpower_gt_0; unfold d1; lia.
@@ -1404,7 +1469,12 @@ Proof.
   case (to_Z_bounded x); intros H1x H2x.
   case (to_Z_bounded (bit x 0)); intros H1b H2b.
   assert (F1: 0 <= [|x >> 1|] < wB/2).
-    rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+    rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
+    {
+      apply Z_div_pos.
+      - apply Zgt_pos_0.
+      - assumption.
+    }
     apply Zdiv_lt_upper_bound; auto with zarith.
   rewrite (bit_split x) at 1.
   rewrite add_spec, Zmod_small, lsl_spec, to_Z_1, Zpower_1_r, Zmod_small;
@@ -1435,9 +1505,19 @@ Proof.
  rewrite (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)).
  assert ([|y>>1|] <= [|(x lor y) >> 1|]).
   rewrite lor_lsr, <-leb_spec; apply IH.
-  rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+  rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
+  {
+    apply Z_div_pos.
+    - apply Zgt_pos_0.
+    - abstract omega.
+  }
   apply Zdiv_lt_upper_bound; auto with zarith.
-  rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+  rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
+  {
+    apply Z_div_pos.
+    - apply Zgt_pos_0.
+    - abstract omega.
+  }
   apply Zdiv_lt_upper_bound; auto with zarith.
  assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith.
  rewrite lor_spec; do 2 case bit; try discriminate.
@@ -1462,9 +1542,19 @@ Proof.
  intros Hn.
  assert (F1: ((x >> 1) + (y >> 1))%int = (x >> 1) lor (y >> 1)).
    apply IH.
-   rewrite lsr_spec, Zpower_1_r; split; auto with zarith.
+   rewrite lsr_spec, Zpower_1_r; split.
+   {
+     apply Z_div_pos.
+     - apply Zgt_pos_0.
+     - abstract omega.
+   }
    apply Zdiv_lt_upper_bound; auto with zarith.
-   rewrite lsr_spec, Zpower_1_r; split; auto with zarith.
+   rewrite lsr_spec, Zpower_1_r; split.
+   {
+     apply Z_div_pos.
+     - apply Zgt_pos_0.
+     - abstract omega.
+   }
    apply Zdiv_lt_upper_bound; auto with zarith.
    intros m H1 H2.
    case_eq (digits <= m)%int;  [idtac | rewrite <- not_true_iff_false];
@@ -1501,9 +1591,19 @@ Proof.
   rewrite Zpower_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith.
   generalize F3; do 2 case bit; try discriminate; auto.
  case (IH (x >> 1) (y >> 1)).
- rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+ rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
+ {
+   apply Z_div_pos.
+   - apply Zgt_pos_0.
+   - abstract omega.
+ }
  apply Zdiv_lt_upper_bound; auto with zarith.
- rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+ rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
+ {
+   apply Z_div_pos.
+   - apply Zgt_pos_0.
+   - abstract omega.
+ }
  apply Zdiv_lt_upper_bound; auto with zarith.
  intros _ HH m; case (to_Z_bounded m); intros H1m H2m.
  case_eq (digits <= m)%int.
@@ -1521,7 +1621,14 @@ Proof.
  rewrite lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; auto with zarith.
  case (to_Z_bounded (x lor y)); intros H1xy H2xy.
  rewrite lsr_spec, to_Z_1, Zpower_1_r; auto with zarith.
- change wB with ((wB/2)*2); split; auto with zarith.
+ change wB with ((wB/2)*2); split.
+ {
+   apply Z.mul_nonneg_nonneg.
+   - apply Z_div_pos.
+     + apply Zgt_pos_0.
+     + assumption.
+   - apply Pos2Z.is_nonneg.
+ }
  assert ([|x lor y|] / 2  < wB / 2); auto with zarith.
  apply Zdiv_lt_upper_bound; auto with zarith.
  split.
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index ee7f119..e47c530 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -10,14 +10,8 @@
 ## To generate the Makefile:                                          ##
 ##   coq_makefile -f Make -o Makefile                                 ##
 ## In the Makefile :                                                  ##
-## 1) Suppress the "Makefile" target                                  ##
-## 2) Change the "all" target:                                        ##
-##    remove the "test", "ztest", "vtest", "lfsctest" and "./"        ##
-##    dependencies                                                    ##
-## 3) Change the "install" and "clean" targets:                       ##
-##    Suppress the "+" lines                                          ##
-## 4) Add to the "clean" target:                                      ##
-##    - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml ##
+## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...)     ##
+## 2) remove "post-all" from the targets "all" and "all.timing.diff"  ##
 ########################################################################
 
 
@@ -41,7 +35,7 @@
 
 -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
 
--extra "test" "" "cd ../unit-tests; make" ""
+-extra "test" "" "cd ../unit-tests; make"
 -extra "ztest" "" "cd ../unit-tests; make zchaff"
 -extra "vtest" "" "cd ../unit-tests; make verit"
 -extra "lfsctest" "" "cd ../unit-tests; make lfsc"
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index f71b0c8..2337ad7 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -1,712 +1,782 @@
-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.6.1      ##
-#############################################################################
-
-# WARNING
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq 8.7.2
+
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include Makefile.conf
+
+# Put in place old names
+VFILES            := $(COQMF_VFILES)
+MLIFILES          := $(COQMF_MLIFILES)
+MLFILES           := $(COQMF_MLFILES)
+ML4FILES          := $(COQMF_ML4FILES)
+MLPACKFILES       := $(COQMF_MLPACKFILES)
+MLLIBFILES        := $(COQMF_MLLIBFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS        := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS         := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS       := $(COQMF_SRC_SUBDIRS)
+COQLIBS           := $(COQMF_COQLIBS)
+COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
+LOCAL             := $(COQMF_LOCAL)
+COQLIB            := $(COQMF_COQLIB)
+DOCDIR            := $(COQMF_DOCDIR)
+OCAMLFIND         := $(COQMF_OCAMLFIND)
+CAMLP4            := $(COQMF_CAMLP4)
+CAMLP4O           := $(COQMF_CAMLP4O)
+CAMLP4BIN         := $(COQMF_CAMLP4BIN)
+CAMLP4LIB         := $(COQMF_CAMLP4LIB)
+CAMLP4OPTIONS     := $(COQMF_CAMLP4OPTIONS)
+CAMLFLAGS         := $(COQMF_CAMLFLAGS)
+HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+
+Makefile.conf: Make
+	coq_makefile -f Make -o Makefile
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include Makefile.local
+
+# Parameters ##################################################################
 #
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in Makefile.local once an for all.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+# Use /usr/bin/env time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=time
+endif
+endif
+else
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+endif
 
+# Coq binaries
+COQC     ?= "$(COQBIN)coqc"
+COQTOP   ?= "$(COQBIN)coqtop"
+COQCHK   ?= "$(COQBIN)coqchk"
+COQDEP   ?= "$(COQBIN)coqdep"
+GALLINA  ?= "$(COQBIN)gallina"
+COQDOC   ?= "$(COQBIN)coqdoc"
+COQMKTOP ?= "$(COQBIN)coqmktop"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+# Timing scripts
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+BEFORE ?=
+AFTER ?=
+
+# FIXME this should be generated by Coq (modules already linked by Coq)
+CAMLDONTLINK=camlp5.gramlib,unix,str
+
+# OCaml binaries
+CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
+CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
+CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -native -slash -ml-synonym .ml4 -ml-synonym .mlpack
+
+# DESTDIR is prepended to all installation paths
+DESTDIR ?=
+
+# Debug builds, typically -g to OCaml, -debug to Coq.
+CAMLDEBUG ?=
+COQDEBUG ?=
+
+# Extra packages to be linked in (as in findlib -package)
+CAMLPKGS ?=
+
+# Option for making timing files
+TIMING?=
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+
+########## End of parameters ##################################################
+# What follows may be relevant to you only if you need to
+# extend this Makefile.  If so, look for 'Extension point' here and
+# put in Makefile.local double colon rules accordingly.
+# E.g. to perform some work after the all target completes you can write
+#
+# post-all::
+# 	echo "All done!"
 #
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
+# in Makefile.local
 #
+###############################################################################
+
 
-.DEFAULT_GOAL := all
 
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# TIMECMD set a command to log .v compilation time;
-# TIMED if non empty, use the default time command as TIMECMD;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-# VERBOSE to disable the short display of compilation rules.
 
-VERBOSE?=
+# Flags #######################################################################
+#
+# We define a bunch of variables combining the parameters
+
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
 
-# Here is a hack to make $(eval $(shell works:
-define donewline
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
+OPT?=
 
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cma
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
 
-TIMED?=
-TIMECMD?=
-STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
+COQCHKFLAGS?=-silent -o $(COQLIBS)
+COQDOCFLAGS?=-interpolate -utf8
+COQDOCLIBS?=$(COQLIBS_NOML)
 
-vo_to_obj = $(addsuffix .o,\
-  $(filter-out Warning: Error:,\
-  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
-
-##########################
-#                        #
-# Libraries definitions. #
-#                        #
-##########################
-
-OCAMLLIBS?=-I "."\
-  -I "bva"\
-  -I "classes"\
-  -I "array"\
-  -I "cnf"\
-  -I "euf"\
-  -I "lfsc"\
-  -I "lia"\
-  -I "smtlib2"\
-  -I "trace"\
-  -I "verit"\
-  -I "zchaff"\
-  -I "versions/standard"\
-  -I "versions/standard/Int63"\
-  -I "versions/standard/Array"\
-  -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
-COQLIBS?=\
-  -R "." SMTCoq\
-  -I "."\
-  -I "bva"\
-  -I "classes"\
-  -I "array"\
-  -I "cnf"\
-  -I "euf"\
-  -I "lfsc"\
-  -I "lia"\
-  -I "smtlib2"\
-  -I "trace"\
-  -I "verit"\
-  -I "zchaff"\
-  -I "versions/standard"\
-  -I "versions/standard/Int63"\
-  -I "versions/standard/Array"\
-  -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
-COQCHKLIBS?=\
-  -R "." SMTCoq
-COQDOCLIBS?=\
-  -R "." SMTCoq
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-CAMLLEX=$(CAMLBIN)ocamllex
-CAMLYACC=$(CAMLBIN)ocamlyacc
+# The version of Coq being run and the version of coq_makefile that
+# generated this makefile
+COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
+COQMAKEFILE_VERSION:=8.7.2
 
-OPT?=
-COQDEP?="$(COQBIN)coqdep" -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(TIMER) "$(COQBIN)coqc"
-GALLINA?="$(COQBIN)gallina"
-COQDOC?="$(COQBIN)coqdoc"
-COQCHK?="$(COQBIN)coqchk"
-COQMKTOP?="$(COQBIN)coqmktop"
-
-COQSRCLIBS?=-I "$(COQLIB)kernel" \
--I "$(COQLIB)lib" \
--I "$(COQLIB)library" \
--I "$(COQLIB)parsing" \
--I "$(COQLIB)pretyping" \
--I "$(COQLIB)interp" \
--I "$(COQLIB)printing" \
--I "$(COQLIB)intf" \
--I "$(COQLIB)proofs" \
--I "$(COQLIB)tactics" \
--I "$(COQLIB)tools" \
--I "$(COQLIB)ltacprof" \
--I "$(COQLIB)toplevel" \
--I "$(COQLIB)stm" \
--I "$(COQLIB)grammar" \
--I "$(COQLIB)config" \
--I "$(COQLIB)ltac" \
--I "$(COQLIB)engine" \
- \
-  -I "$(COQLIB)/plugins/btauto" \
-  -I "$(COQLIB)/plugins/cc" \
-  -I "$(COQLIB)/plugins/decl_mode" \
-  -I "$(COQLIB)/plugins/derive" \
-  -I "$(COQLIB)/plugins/extraction" \
-  -I "$(COQLIB)/plugins/firstorder" \
-  -I "$(COQLIB)/plugins/fourier" \
-  -I "$(COQLIB)/plugins/funind" \
-  -I "$(COQLIB)/plugins/ltac" \
-  -I "$(COQLIB)/plugins/micromega" \
-  -I "$(COQLIB)/plugins/nsatz" \
-  -I "$(COQLIB)/plugins/omega" \
-  -I "$(COQLIB)/plugins/quote" \
-  -I "$(COQLIB)/plugins/romega" \
-  -I "$(COQLIB)/plugins/rtauto" \
-  -I "$(COQLIB)/plugins/setoid_ring" \
-  -I "$(COQLIB)/plugins/ssrmatching" \
-  -I "$(COQLIB)/plugins/syntax" \
-  -I "$(COQLIB)/plugins/xml"
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-
-CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread
-CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread
-CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread
-CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread
-CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
-CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)
-GRAMMARS?=grammar.cma
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+
+# ocamldoc fails with unknown argument otherwise
+CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+
+# FIXME This should be generated by Coq
+GRAMMARS:=grammar.cma
 ifeq ($(CAMLP4),camlp5)
 CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
 else
 CAMLP4EXTEND=
 endif
-PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \
-  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
-
-##################
-#                #
-# Install Paths. #
-#                #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?="$(HOME)/.local/share"
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL="${COQLIB}user-contrib"
-COQDOCINSTALL="${DOCDIR}user-contrib"
-COQTOPINSTALL="${COQLIB}toploop"
-endif
 
-######################
-#                    #
-# Files dispatching. #
-#                    #
-######################
-
-VFILES:=versions/standard/Int63/Int63.v\
-  versions/standard/Int63/Int63Native.v\
-  versions/standard/Int63/Int63Op.v\
-  versions/standard/Int63/Int63Axioms.v\
-  versions/standard/Int63/Int63Properties.v\
-  versions/standard/Array/PArray.v\
-  versions/standard/Structures.v\
-  bva/BVList.v\
-  bva/Bva_checker.v\
-  classes/SMT_classes.v\
-  classes/SMT_classes_instances.v\
-  array/FArray.v\
-  array/Array_checker.v\
-  cnf/Cnf.v\
-  euf/Euf.v\
-  lia/Lia.v\
-  spl/Assumptions.v\
-  spl/Syntactic.v\
-  spl/Arithmetic.v\
-  spl/Operators.v\
-  Conversion_tactics.v\
-  Misc.v\
-  SMTCoq.v\
-  ReflectFacts.v\
-  PropToBool.v\
-  BoolToProp.v\
-  Tactics.v\
-  SMT_terms.v\
-  State.v\
-  Trace.v
-
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(VFILES))
+CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null)
+ifeq (,$(CAMLLIB))
+PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.")
 else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(VFILES))
-endif
+PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
 endif
 
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-VO=vo
-VOFILES:=$(VFILES:.v=.$(VO))
-GLOBFILES:=$(VFILES:.v=.glob)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES=$(call vo_to_obj,$(VOFILES))
-ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
-NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ML4FILES:=g_smtcoq.ml4
-
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(ML4FILES))
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
 else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(ML4FILES))
+TIMING_EXT=timing
 endif
 endif
-
-.SECONDARY: $(addsuffix .d,$(ML4FILES))
-
-MLFILES:=versions/standard/structures.ml\
-  trace/coqTerms.ml\
-  trace/smtBtype.ml\
-  trace/satAtom.ml\
-  trace/smtAtom.ml\
-  trace/smtCertif.ml\
-  trace/smtCnf.ml\
-  trace/smtCommands.ml\
-  trace/smtForm.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_util.ml\
-  smtlib2/sExpr.ml\
-  smtlib2/smtlib2_solver.ml\
-  smtlib2/sExprParser.ml\
-  smtlib2/sExprLexer.ml\
-  verit/veritParser.ml\
-  verit/veritLexer.ml\
-  verit/verit.ml\
-  verit/veritSyntax.ml\
-  lfsc/shashcons.ml\
-  lfsc/hstring.ml\
-  lfsc/lfscParser.ml\
-  lfsc/type.ml\
-  lfsc/ast.ml\
-  lfsc/builtin.ml\
-  lfsc/tosmtcoq.ml\
-  lfsc/converter.ml\
-  lfsc/lfsc.ml\
-  lfsc/lfscLexer.ml\
-  zchaff/cnfParser.ml\
-  zchaff/satParser.ml\
-  zchaff/zchaff.ml\
-  zchaff/zchaffParser.ml\
-  lia/lia.ml
-
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(MLFILES))
 else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(MLFILES))
+TIMING_ARG=
 endif
+
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
 endif
 
-.SECONDARY: $(addsuffix .d,$(MLFILES))
+concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2))
 
-MLPACKFILES:=smtcoq_plugin.mlpack
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
 
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(MLPACKFILES))
+# Files #######################################################################
+#
+# We here define a bunch of variables about the files being part of the
+# Coq project in order to ease the writing of build target and build rules
+
+ALLSRCFILES := \
+	$(VFILES) \
+	$(ML4FILES) \
+	$(MLFILES) \
+	$(MLPACKFILES) \
+	$(MLLIBFILES) \
+	$(MLIFILES)
+
+# helpers
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
+strip_dotslash = $(patsubst ./%,%,$(1))
+VO = vo
+
+VOFILES = $(VFILES:.v=.$(VO))
+GLOBFILES = $(VFILES:.v=.glob)
+GFILES = $(VFILES:.v=.g)
+HTMLFILES = $(VFILES:.v=.html)
+GHTMLFILES = $(VFILES:.v=.g.html)
+BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
+TEXFILES = $(VFILES:.v=.tex)
+GTEXFILES = $(VFILES:.v=.g.tex)
+CMOFILES = \
+	$(ML4FILES:.ml4=.cmo) \
+	$(MLFILES:.ml=.cmo) \
+	$(MLPACKFILES:.mlpack=.cmo)
+CMXFILES = $(CMOFILES:.cmo=.cmx)
+OFILES = $(CMXFILES:.cmx=.o)
+CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
+CMXAFILES = $(CMAFILES:.cma=.cmxa)
+CMIFILES = \
+	$(CMOFILES:.cmo=.cmi) \
+	$(MLIFILES:.mli=.cmi)
+# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
+# a .ml4 file
+CMXSFILES = \
+	$(MLPACKFILES:.mlpack=.cmxs) \
+	$(CMXAFILES:.cmxa=.cmxs) \
+	$(if $(MLPACKFILES)$(CMXAFILES),,\
+		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+
+# files that are packed into a plugin (no extension)
+PACKEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib))))
+# files that are archived into a .cma (mllib)
+LIBEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib))))
+CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
+CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
+OBJFILES = $(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES = \
+	$(OBJFILES:.o=.cmi) \
+	$(OBJFILES:.o=.cmx) \
+	$(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files, so that `install` doesn't show
+# warnings and `clean` doesn't pass to rm a list of files that is too long for
+# the shell.
+NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
+FILESTOINSTALL = \
+	$(VOFILES) \
+	$(VFILES) \
+	$(GLOBFILES) \
+	$(NATIVEFILES) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
+	$(CMOFILESTOINSTALL) \
+	$(CMAFILES)
+ifeq '$(HASNATDYNLINK)' 'true'
+DO_NATDYNLINK = yes
+FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
 else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(MLPACKFILES))
-endif
+DO_NATDYNLINK =
 endif
 
-.SECONDARY: $(addsuffix .d,$(MLPACKFILES))
-
-MLIFILES:=versions/standard/structures.mli\
-  trace/coqTerms.mli\
-  trace/smtBtype.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\
-  smtlib2/sExpr.mli\
-  smtlib2/smtlib2_solver.mli\
-  smtlib2/sExprParser.mli\
-  verit/veritParser.mli\
-  verit/veritLexer.mli\
-  verit/verit.mli\
-  verit/veritSyntax.mli\
-  lfsc/shashcons.mli\
-  lfsc/hstring.mli\
-  lfsc/lfscParser.mli\
-  lfsc/ast.mli\
-  lfsc/translator_sig.mli\
-  lfsc/tosmtcoq.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))
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES))
+
+# Compilation targets #########################################################
+
+all:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+.PHONY: all
+
+all.timing.diff:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
+.PHONY: all.timing.diff
+
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
 else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(MLIFILES))
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 endif
 endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
 
-.SECONDARY: $(addsuffix .d,$(MLIFILES))
+# Extension points for actions to be performed before/after the all target
+pre-all::
+	@# Extension point
+	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
+	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	fi
+.PHONY: pre-all
 
-ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)
-CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
-CMXFILES=$(CMOFILES:.cmo=.cmx)
-OFILES=$(CMXFILES:.cmx=.o)
-CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))
-CMXSFILES=$(CMXFILES:.cmx=.cmxs)
-ifeq '$(HASNATDYNLINK)' 'true'
-HASNATDYNLINK_OR_EMPTY := yes
-else
-HASNATDYNLINK_OR_EMPTY :=
-endif
+post-all::
+	@# Extension point
+.PHONY: post-all
 
-#######################################
-#                                     #
-# Definition of the toplevel targets. #
-#                                     #
-#######################################
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
+.PHONY: real-all
 
-all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES))
+real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
+.PHONE: real-all.timing.diff
 
-mlihtml: $(MLIFILES:.mli=.cmi)
-	 mkdir $@ || rm -rf $@/*
-	$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
 
-all-mli.tex: $(MLIFILES:.mli=.cmi)
-	$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
 
+# FIXME, see Ralph's bugreport
 quick: $(VOFILES:.vo=.vio)
+.PHONY: quick
 
 vio2vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-checkproofs:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
 
-all.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+checkproofs:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: checkproofs
 
 validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
+.PHONY: validate
 
-beautify: $(VFILES:=.beautified)
-	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
-	@echo 'Do not do "make clean" until you are sure that everything went well!'
-	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+only: $(TGTS)
+.PHONY: only
 
-.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo ./ smtcoq_plugin.mlpack.d
+# Documentation targets #######################################################
 
-###################
-#                 #
-# Custom targets. #
-#                 #
-###################
-
-test: 
-	cd ../unit-tests; make
-
-ztest: 
-	cd ../unit-tests; make zchaff
-
-vtest: 
-	cd ../unit-tests; make verit
-
-lfsctest: 
-	cd ../unit-tests; make lfsc
-
-%.ml: %.mll
-	$(CAMLLEX) $<
-
-%.ml %.mli: %.mly
-	$(CAMLYACC) $<
-
-smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
+html: $(GLOBFILES) $(VFILES)
+	$(SHOW)'COQDOC -d html $(GAL)'
+	$(HIDE)mkdir -p html
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
 
-###################
-#                 #
-# Subdirectories. #
-#                 #
-###################
+mlihtml: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -d $@'
+	$(HIDE)mkdir $@ || rm -rf $@/*
+	$(HIDE)$(CAMLDOC) -html \
+		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
 
-./:
-	+cd "./" && $(MAKE) all
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -latex $@'
+	$(HIDE)$(CAMLDOC) -latex \
+		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
 
-#####################################
-#                                   #
-# Ad-hoc implicit rules for mlpack. #
-#                                   #
-#####################################
+gallina: $(GFILES)
 
-$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml
-	$(SHOW)'CAMLOPT -c -for-pack Smtcoq_plugin $<'
-	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $<
+all.ps: $(VFILES)
+	$(SHOW)'COQDOC -ps $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
 
-$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml4
-	$(SHOW)'CAMLOPT -c -pp -for-pack Smtcoq_plugin $<'
-	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $(PP) -impl $<
+all.pdf: $(VFILES)
+	$(SHOW)'COQDOC -pdf $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
 
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
+# FIXME: not quite right, since the output name is different
+gallinahtml: GAL=-g
+gallinahtml: html
 
-byte:
-	$(MAKE) all "OPT:=-byte"
+all-gal.ps: GAL=-g
+all-gal.ps: all.ps
 
-opt:
-	$(MAKE) all "OPT:=-opt"
+all-gal.pdf: GAL=-g
+all-gal.pdf: all.pdf
 
-userinstall:
-	+$(MAKE) USERINSTALL=true install
+# ?
+beautify: $(BEAUTYFILES)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+.PHONY: beautify
 
-install-natdynlink:
-	cd "." && for i in $(CMXSFILES); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
-	 install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
+# Installation targets ########################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
+
+install:
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
 	done
-
-install-toploop: $(MLLIBFILES:.mllib=.cmxs)
-	 install -d "$(DSTROOT)"$(COQTOPINSTALL)/
-	 install -m 0755 $?  "$(DSTROOT)"$(COQTOPINSTALL)/
-
-install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)
-	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
+	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+install-extra::
+	@# Extension point
+.PHONY: install install-extra
+
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
 	done
 
-install-doc:
-	install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html
-	for i in html/*; do \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\
+install-doc:: html mlihtml
+	@# Extension point
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)for i in html/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
 	done
-	install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/mlihtml
-	for i in mlihtml/*; do \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\
+	$(HIDE)install -d \
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)for i in mlihtml/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
 	done
-
-uninstall_me.sh: Makefile
-	echo '#!/bin/sh' > $@
-	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(CMXSFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@"
-	printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@"
-	printf '&& rm -f $(shell find "mlihtml" -maxdepth 1 -and -type f -print)\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/mlihtml -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	chmod +x $@
-
-uninstall: uninstall_me.sh
-	sh $<
-
-.merlin:
-	@echo 'FLG -rectypes' > .merlin
-	@echo "B $(COQLIB)kernel" >> .merlin
-	@echo "B $(COQLIB)lib" >> .merlin
-	@echo "B $(COQLIB)library" >> .merlin
-	@echo "B $(COQLIB)parsing" >> .merlin
-	@echo "B $(COQLIB)pretyping" >> .merlin
-	@echo "B $(COQLIB)interp" >> .merlin
-	@echo "B $(COQLIB)printing" >> .merlin
-	@echo "B $(COQLIB)intf" >> .merlin
-	@echo "B $(COQLIB)proofs" >> .merlin
-	@echo "B $(COQLIB)tactics" >> .merlin
-	@echo "B $(COQLIB)tools" >> .merlin
-	@echo "B $(COQLIB)ltacprof" >> .merlin
-	@echo "B $(COQLIB)toplevel" >> .merlin
-	@echo "B $(COQLIB)stm" >> .merlin
-	@echo "B $(COQLIB)grammar" >> .merlin
-	@echo "B $(COQLIB)config" >> .merlin
-	@echo "B $(COQLIB)ltac" >> .merlin
-	@echo "B $(COQLIB)engine" >> .merlin
-	@echo "B /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin
-	@echo "S /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin
-	@echo "B bva" >> .merlin
-	@echo "S bva" >> .merlin
-	@echo "B classes" >> .merlin
-	@echo "S classes" >> .merlin
-	@echo "B array" >> .merlin
-	@echo "S array" >> .merlin
-	@echo "B cnf" >> .merlin
-	@echo "S cnf" >> .merlin
-	@echo "B euf" >> .merlin
-	@echo "S euf" >> .merlin
-	@echo "B lfsc" >> .merlin
-	@echo "S lfsc" >> .merlin
-	@echo "B lia" >> .merlin
-	@echo "S lia" >> .merlin
-	@echo "B smtlib2" >> .merlin
-	@echo "S smtlib2" >> .merlin
-	@echo "B trace" >> .merlin
-	@echo "S trace" >> .merlin
-	@echo "B verit" >> .merlin
-	@echo "S verit" >> .merlin
-	@echo "B zchaff" >> .merlin
-	@echo "S zchaff" >> .merlin
-	@echo "B versions/standard" >> .merlin
-	@echo "S versions/standard" >> .merlin
-	@echo "B versions/standard/Int63" >> .merlin
-	@echo "S versions/standard/Int63" >> .merlin
-	@echo "B versions/standard/Array" >> .merlin
-	@echo "S versions/standard/Array" >> .merlin
-	@echo "B $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin
-	@echo "S $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin
+.PHONY: install-doc
+
+uninstall::
+	@# Extension point
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 rm -f "$$instf" &&\
+	 echo RM "$$instf" &&\
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	done
+.PHONY: uninstall
+
+uninstall-doc::
+	@# Extension point
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+.PHONY: uninstall-doc
+
+# Cleaning ####################################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
 
 clean::
-	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
-	rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
-	rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))
-	rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
-	find . -name .coq-native -type d -empty -delete
-	rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
-	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
-	- rm -rf html mlihtml uninstall_me.sh
-	- rm -rf test
-	- rm -rf ztest
-	- rm -rf vtest
-	- rm -rf lfsctest
-	- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml
+	@# Extension point
+	$(SHOW)'CLEAN'
+	$(HIDE)rm -f $(CMOFILES)
+	$(HIDE)rm -f $(CMIFILES)
+	$(HIDE)rm -f $(CMAFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXAFILES)
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(ALLDFILES)
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)find . -name .coq-native -type d -empty -delete
+	$(HIDE)rm -f $(VOFILES)
+	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(GFILES)
+	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
+	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
+	$(HIDE)rm -f $(VFILES:.v=.glob)
+	$(HIDE)rm -f $(VFILES:.v=.tex)
+	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)rm -rf html mlihtml
+.PHONY: clean
 
 cleanall:: clean
-	rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	@# Extension point
+	$(SHOW)'CLEAN *.aux *.timing'
+	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	$(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
+.PHONY: cleanall
 
 archclean::
-	rm -f *.cmx *.o
-	+cd ./ && $(MAKE) archclean
+	@# Extension point
+	$(SHOW)'CLEAN *.cmx *.o'
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+.PHONY: archclean
 
-printenv:
-	@"$(COQBIN)coqtop" -config
-	@echo 'OCAMLFIND =	$(OCAMLFIND)'
-	@echo 'PP =	$(PP)'
-	@echo 'COQFLAGS =	$(COQFLAGS)'
-	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
-	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
 
-
-###################
-#                 #
-# Implicit rules. #
-#                 #
-###################
+# Compilation rules ###########################################################
 
 $(MLIFILES:.mli=.cmi): %.cmi: %.mli
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
-	$(SHOW)'CAMLDEP $<'
-	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
 
 $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
 	$(SHOW)'CAMLC -pp -c $<'
-	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $<
 
-$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4
-	$(SHOW)'CAMLOPT -pp -c $<'
-	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
-	$(SHOW)'CAMLDEP -pp $<'
-	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
+	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
 
 $(MLFILES:.ml=.cmo): %.cmo: %.ml
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
 
-$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml
-	$(SHOW)'CAMLOPT -c $<'
-	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
+$(MLFILES:.ml=.cmx): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
 
-$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
-	$(SHOW)'CAMLDEP $<'
-	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-linkall -shared -o $@ $<
 
-$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
 	$(SHOW)'CAMLC -pack -o $@'
-	$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(SHOW)'CAMLOPT -pack -o $@'
-	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
-$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
-	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+# This rule is for _CoqProject with no .mllib nor .mlpack
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -o $@ $<
+
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
 
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
 
+# FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
-	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+	$(SHOW)COQC -quick $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+$(BEAUTYFILES): %.v.beautified: %.v
+	$(SHOW)'BEAUTIFY $<'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
 
 $(GFILES): %.g: %.v
-	$(GALLINA) $<
+	$(SHOW)'GALLINA $<'
+	$(HIDE)$(GALLINA) $<
 
-$(VFILES:.v=.tex): %.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+$(TEXFILES): %.tex: %.v
+	$(SHOW)'COQDOC -latex $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
 
-$(HTMLFILES): %.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+$(GTEXFILES): %.g.tex: %.v
+	$(SHOW)'COQDOC -latex -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
 
-$(VFILES:.v=.g.tex): %.g.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+$(HTMLFILES): %.html: %.v %.glob
+	$(SHOW)'COQDOC -html $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
 
 $(GHTMLFILES): %.g.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+	$(SHOW)'COQDOC -html -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+# Dependency files ############################################################
+
+ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
+ -include $(ALLDFILES)
+else
+ ifeq ($(MAKECMDGOALS),)
+  -include $(ALLDFILES)
+ endif
+endif
+
+.SECONDARY: $(ALLDFILES)
+
+redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
+
+$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
+	$(SHOW)'CAMLDEP -pp $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
 
 $(addsuffix .d,$(VFILES)): %.v.d: %.v
 	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok)
 
-$(addsuffix .beautified,$(VFILES)): %.v.beautified:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
+# Misc ########################################################################
 
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
+byte:
+	$(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
+.PHONY: byte
 
+opt:
+	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
+.PHONY:	opt
+
+# This is deprecated.  To extend this makefile use
+# extension points and Makefile.local
+printenv::
+	$(warning printenv is deprecated)
+	$(warning write extensions in Makefile.local or include Makefile.conf)
+	@echo 'LOCAL = $(LOCAL)'
+	@echo 'COQLIB = $(COQLIB)'
+	@echo 'DOCDIR = $(DOCDIR)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'CAMLP4 = $(CAMLP4)'
+	@echo 'CAMLP4O = $(CAMLP4O)'
+	@echo 'CAMLP4BIN = $(CAMLP4BIN)'
+	@echo 'CAMLP4LIB = $(CAMLP4LIB)'
+	@echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)'
+	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
+	@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
+	@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'PP = $(PP)'
+	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+.PHONY:	printenv
+
+# Generate a .merlin file.  If you need to append directives to this
+# file you can extend the merlin-hook target in Makefile.local
+.merlin:
+	$(SHOW)'FILL .merlin'
+	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
+	$(HIDE)echo 'B $(COQLIB)' >> .merlin
+	$(HIDE)echo 'S $(COQLIB)' >> .merlin
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'B $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'S $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
+	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
+.PHONY: merlin
+
+merlin-hook::
+	@# Extension point
+.PHONY: merlin-hook
+
+# prints all variables
+debug:
+	$(foreach v,\
+		$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
+	       		$(.VARIABLES))),\
+	       	$(info $(v) = $($(v))))
+.PHONY: debug
+
+.DEFAULT_GOAL := all
diff --git a/src/versions/standard/Makefile.conf b/src/versions/standard/Makefile.conf
new file mode 100644
index 0000000..928db7d
--- /dev/null
+++ b/src/versions/standard/Makefile.conf
@@ -0,0 +1,103 @@
+# This configuration file was generated by running:
+# coq_makefile -f Make -o Makefile
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = versions/standard/Int63/Int63.v versions/standard/Int63/Int63Native.v versions/standard/Int63/Int63Op.v versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Properties.v versions/standard/Array/PArray.v versions/standard/Structures.v bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v lia/Lia.v spl/Assumptions.v spl/Syntactic.v spl/Arithmetic.v spl/Operators.v Conversion_tactics.v Misc.v SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v Tactics.v SMT_terms.v State.v Trace.v
+COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.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 smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli
+COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.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_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml
+COQMF_ML4FILES = g_smtcoq.ml4
+COQMF_MLPACKFILES = smtcoq_plugin.mlpack
+COQMF_MLLIBFILES = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega'
+COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega'
+COQMF_COQLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega'  -R . SMTCoq
+COQMF_COQLIBS_NOML =  -R . SMTCoq
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=1
+COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2//
+COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/
+COQMF_OCAMLFIND=/usr/bin/ocamlfind
+COQMF_CAMLP4=camlp5
+COQMF_CAMLP4O=/usr/bin/camlp5o
+COQMF_CAMLP4BIN=/usr/bin/
+COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5
+COQMF_CAMLP4OPTIONS=-loc loc
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50  -safe-string
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
+COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+CAMLLEX = $(CAMLBIN)ocamllex
+CAMLYACC = $(CAMLBIN)ocamlyacc
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = SMTCoq
+
+###############################################################################
+#                                                                             #
+# Extra targets. (-extra and -extra-phony, DEPRECATED)                        #
+#                                                                             #
+###############################################################################
+
+post-all::
+	$(MAKE) -f $(SELF) test
+clean::
+	rm -f test
+test :  
+	cd ../unit-tests; make
+
+post-all::
+	$(MAKE) -f $(SELF) ztest
+clean::
+	rm -f ztest
+ztest :  
+	cd ../unit-tests; make zchaff
+
+post-all::
+	$(MAKE) -f $(SELF) vtest
+clean::
+	rm -f vtest
+vtest :  
+	cd ../unit-tests; make verit
+
+post-all::
+	$(MAKE) -f $(SELF) lfsctest
+clean::
+	rm -f lfsctest
+lfsctest :  
+	cd ../unit-tests; make lfsc
+
+%.ml :  %.mll
+	$(CAMLLEX) $<
+
+%.ml %.mli :  %.mly
+	$(CAMLYACC) $<
+
+.PHONY: smtcoq_plugin.mlpack.d
+smtcoq_plugin.mlpack.d :  verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
+	
+
diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v
index 4894ebd..d6c4435 100644
--- a/src/versions/standard/Structures_standard.v
+++ b/src/versions/standard/Structures_standard.v
@@ -50,6 +50,15 @@ Section Trace.
 End Trace.
 
 
+Require Import PeanoNat.
+
 Definition nat_eqb := Nat.eqb.
 Definition nat_eqb_eq := Nat.eqb_eq.
 Definition nat_eqb_refl := Nat.eqb_refl.
+
+
+(*
+   Local Variables:
+   coq-load-path: ((rec "../.." "SMTCoq"))
+   End:
+*)
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
index 2cc4415..bf923cc 100644
--- a/src/versions/standard/g_smtcoq_standard.ml4
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -12,9 +12,12 @@
 
 DECLARE PLUGIN "smtcoq_plugin"
 
-open Genarg
 open Stdarg
-open Constrarg
+
+(* This is requires since Coq 8.7 because the Ltac machinery became a
+   plugin
+   see: https://lists.gforge.inria.fr/pipermail/coq-commits/2017-February/021276.html *)
+open Ltac_plugin
 
 VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY
 | [ "Parse_certif_zchaff" 
@@ -86,8 +89,8 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ]
-| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check lpl !lemmas_list ]
+| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ]
+| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ]
 END
 
 TACTIC EXTEND Tactic_cvc4
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index cf5a272..74caf8b 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -11,10 +11,12 @@
 
 
 open Entries
-open Coqlib
 
 
+(* Constr generation and manipulation *)
+
 let mklApp f args = Term.mkApp (Lazy.force f, args)
+let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n
 let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 
@@ -75,17 +77,15 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
 
 
 (* Differences between the two versions of Coq *)
-let dummy_loc = Loc.ghost
-
-let mkUConst c =
+let mkUConst : Term.constr -> Safe_typing.private_constants Entries.definition_entry = fun c ->
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let evd, ty = Typing.type_of env evd c in
-  { const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
+  let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
+  { Entries.const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
                                                Safe_typing.empty_private_constants);
     const_entry_secctx      = None;
     const_entry_feedback    = None;
-    const_entry_type        = Some ty;
+    const_entry_type        = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Term.constr *)
     const_entry_polymorphic = false;
     const_entry_universes   = snd (Evd.universe_context evd);
     const_entry_opaque      = false;
@@ -94,7 +94,7 @@ let mkUConst c =
 let mkTConst c noc ty =
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let evd, _ = Typing.type_of env evd noc in
+  let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
   { const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
                                                Safe_typing.empty_private_constants);
     const_entry_secctx      = None;
@@ -105,25 +105,25 @@ let mkTConst c noc ty =
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
-let error = CErrors.error
+let error s = CErrors.user_err (Pp.str s)
 
 let coqtype = Future.from_val Term.mkSet
 
 let declare_new_type t =
-  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in
+  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (None, t) in
   Term.mkVar t
 
 let declare_new_variable v constr_t =
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let evd, _ = Typing.type_of env evd constr_t in
-  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (dummy_loc, v) in
+  let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
+  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (None, v) in
   Term.mkVar v
 
-let extern_constr = Constrextern.extern_constr true Environ.empty_env Evd.empty
+let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
 
 let vernacentries_interp expr =
-  Vernacentries.interp (dummy_loc, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr))
+  Vernacentries.interp (None, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr))
 
 let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
@@ -136,43 +136,60 @@ let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst
 
 let tclTHEN = Tacticals.New.tclTHEN
 let tclTHENLAST = Tacticals.New.tclTHENLAST
-let assert_before = Tactics.assert_before
+let assert_before n c = Tactics.assert_before n (EConstr.of_constr c)
 
 let vm_conv = Vconv.vm_conv
-let vm_cast_no_check t = Tactics.vm_cast_no_check t
+let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c)
+(* Cannot contain evars since it comes from a Term.constr *)
+let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t))
 
-(* Warning 40: this record of type Proofview.Goal.enter contains fields
-   that are not visible in the current scope: enter. *)
 let mk_tactic tac =
-  Proofview.Goal.nf_enter {Proofview.Goal.enter = (fun gl ->
+  Proofview.Goal.nf_enter (fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let t = Proofview.Goal.concl gl in
+    let t = EConstr.to_constr sigma t in (* The goal should not contain uninstanciated evars *)
     tac env sigma t
-  )}
+  )
 let set_evars_tac noc =
   mk_tactic (
       fun env sigma _ ->
-      let sigma, _ = Typing.type_of env sigma noc in
+      let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in
       Proofview.Unsafe.tclEVARS sigma)
 
 let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
-let constrextern_extern_constr =
+let constrextern_extern_constr c =
   let env = Global.env () in
-  Constrextern.extern_constr false env (Evd.from_env env)
+  Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c)
 
 let get_rel_dec_name = function
   | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n
 
+let retyping_get_type_of env sigma c =
+  (* Cannot contain evars since it comes from a Term.constr *)
+  EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))
 
-(* New packaging of plugins *)
+
+(* Micromega *)
 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
 
+let micromega_coq_proofTerm =
+  (* Cannot contain evars *)
+  lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm)))
+
+let micromega_dump_proof_term p =
+  (* Cannot contain evars *)
+  EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p)
+
 
 (* Types in the Coq source code *)
 type tactic = unit Proofview.tactic
 type names_id = Names.Id.t
 type constr_expr = Constrexpr.constr_expr
+
+(* EConstr *)
+type econstr = EConstr.t
+let econstr_of_constr = EConstr.of_constr
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index b17aa3c..3d17203 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -10,8 +10,13 @@
 (**************************************************************************)
 
 
+(* Constr generation and manipulation *)
+(* WARNING: currently, we map all the econstr into constr: we suppose
+   that the goal does not contain existencial variables *)
 val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
 val gen_constant : string list list -> string -> Term.constr lazy_t
+
+(* Int63 *)
 val int63_modules : string list list
 val int31_module : string list list
 val cD0 : Term.constr lazy_t
@@ -19,11 +24,15 @@ val cD1 : Term.constr lazy_t
 val cI31 : Term.constr lazy_t
 val mkInt : int -> Term.constr
 val cint : Term.constr lazy_t
+
+(* PArray *)
 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
+
+(* Traces *)
 val mkTrace :
   ('a -> Term.constr) ->
   ('a -> 'a) ->
@@ -33,7 +42,8 @@ val mkTrace :
   Term.constr Lazy.t ->
   Term.constr Lazy.t ->
   int -> Term.constr -> Term.constr -> 'a ref -> Term.constr
-val dummy_loc : Loc.t
+
+(* Differences between the two versions of Coq *)
 val mkUConst :
   Term.constr -> Safe_typing.private_constants Entries.definition_entry
 val mkTConst :
@@ -55,8 +65,11 @@ val tclTHEN :
 val tclTHENLAST :
   unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
 val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic
+
 val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function
 val vm_cast_no_check : Term.constr -> unit Proofview.tactic
+val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr
+
 val mk_tactic :
   (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) ->
   unit Proofview.tactic
@@ -64,16 +77,24 @@ val set_evars_tac : Term.constr -> unit Proofview.tactic
 val ppconstr_lsimpleconstr : Ppconstr.precedence
 val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr
 val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
 
 
-(* New packaging of plugins *)
+(* Micromega *)
 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
 
+val micromega_coq_proofTerm : Term.constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr
+
 
 (* Types in the Coq source code *)
 type tactic = unit Proofview.tactic
 type names_id = Names.Id.t
 type constr_expr = Constrexpr.constr_expr
+
+(* EConstr *)
+type econstr = EConstr.t
+val econstr_of_constr : Term.constr -> econstr