V8.7 (#36)

Port SMTCoq to Coq-8.7

54 files changed, 1597 insertions, 1259 deletions

diff --git a/.gitignore b/.gitignore
index 3199ccb..b5aaccd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,7 +21,9 @@ setup.log
 .nia.cache
 
 # cp targets of src/configure.sh:
+src/Make
 src/Makefile
+src/Makefile.conf
 src/smtcoq_plugin.ml4
 src/versions/native/Structures.v
 src/g_smtcoq.ml4
diff --git a/INSTALL.md b/INSTALL.md
index 59c40f7..73084c5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -15,7 +15,7 @@ changes](#setting-up-environment-for-smtcoq).
 
 ## Requirements
 
-You need to have OCaml version >= 4.04.0 and Coq version 8.6 or 8.6.1.
+You need to have OCaml version >= 4.04.0 and Coq version 8.7.*.
 The easiest way to install these two pieces of software is through opam.
 
 > **Warning**: The version of Coq that you plan to use must have been compiled
@@ -26,7 +26,7 @@ The easiest way to install these two pieces of software is through opam.
 If you want to use SMTCoq with high performance, you need to use the
 [version of Coq with native
 data-structures](https://github.com/smtcoq/native-coq) instead of
-Coq-8.6.
+Coq-8.7.
 
 
 ### Installation with Coq and OCaml opam packages
@@ -63,16 +63,16 @@ opam switch 4.04.0
 
 #### Install Coq
 
-After OCaml is installed, you can install Coq through opam (we recommend 8.6.1).
+After OCaml is installed, you can install Coq through opam (we recommend 8.7.2).
 
 ```bash
-opam install coq.8.6.1
+opam install coq.8.7.2
 ```
 
 If you also want to install CoqIDE at the same time you can do
 
 ```bash
-opam install coq.8.6.1 coqide.8.6.1
+opam install coq.8.7.2 coqide.8.7.2
 ```
 
 but you might need to install some extra packages and libraries for your system
@@ -90,11 +90,11 @@ make install
 ```
 
 
-### Installation with official Coq 8.6 release
+### Installation with official Coq 8.7 release
 
-1. Download the last stable version of Coq 8.6:
+1. Download the last stable version of Coq 8.7:
 ```bash
-wget https://coq.inria.fr/distrib/8.6.1/files/coq-8.6.1.tar.gz
+wget https://coq.inria.fr/distrib/8.7.2/files/coq-8.7.2.tar.gz
 ```
    and compile it by following the instructions available in the
    repository (make sure you use OCaml 4.04.0 for that). We recommand
@@ -107,7 +107,7 @@ make
 2. Set an environment variable COQBIN to the directory where Coq's
    binaries are; for instance:
 ```bash
-export COQBIN=/home/jdoe/coq-8.6.1/bin/
+export COQBIN=/home/jdoe/coq-8.7.2/bin/
 ```
    (the final slash is mandatory).
 
diff --git a/src/Misc.v b/src/Misc.v
index fe724f4..84feab4 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import Bool List PArray Int63.
+Require Import Bool List PArray Int63 ZArith.
 Local Open Scope int63_scope.
 Local Open Scope array_scope.
 
@@ -1038,3 +1038,10 @@ Proof. destruct b; intuition. Qed.
 
 Lemma is_true_iff e :  e = true <-> is_true e.
 Proof. now unfold is_true. Qed.
+
+
+(* 
+   Local Variables:
+   coq-load-path: ((rec "." "SMTCoq"))
+   End: 
+*)
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index c411c99..c627bc2 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import Bool Int63 PArray BinPos SMT_classes_instances.
+Require Import Bool Int63 PArray BinNat BinPos ZArith SMT_classes_instances.
 Require Import Misc State BVList. (* FArray Equalities DecidableTypeEx. *)
 Require FArray.
 Require List .
@@ -2452,10 +2452,10 @@ Qed.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x + k2 interp_t y)%Z; auto.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x - k2 interp_t y)%Z; auto.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x * k2 interp_t y)%Z; auto.
-        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <? k2 interp_t y); auto.
-        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <=? k2 interp_t y); auto.
-        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >=? k2 interp_t y); auto.
-        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <? k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <=? k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >=? k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y)%Z; auto.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) A); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) A) as [k2| ]; simpl; try (exists true; reflexivity); exists (Typ.i_eqb t_i A (k1 interp_t x) (k2 interp_t y)); auto.
 
         (*BO_BVand*)
@@ -2659,3 +2659,10 @@ Section PredefinedArrays.
 
 End PredefinedArrays.
 *)
+
+
+(* 
+   Local Variables:
+   coq-load-path: ((rec "." "SMTCoq"))
+   End: 
+*)
diff --git a/src/State.v b/src/State.v
index 3125b06..a3af611 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,10 +10,7 @@
 (**************************************************************************)
 
 
-Require Import List.
-Require Import Bool.
-Require Import Int63.
-Require Import PArray.
+Require Import List Bool Int63 PArray Omega.
 
 (* Require Import AxiomesInt. *)
 
diff --git a/src/Tactics.v b/src/Tactics.v
index 68c51dd..106e128 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -11,7 +11,7 @@
 
 
 Require Import PropToBool BoolToProp.  (* Before SMTCoq.State *)
-Require Import Int63 List PArray Bool.
+Require Import Int63 List PArray Bool ZArith.
 Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances.
 
 Declare ML Module "smtcoq_plugin".
@@ -50,15 +50,15 @@ Qed.
 
 (* verit considers equality modulo its symmetry, so we have to recover the
    right direction in the instances of the theorems *)
-Definition hidden_eq a b := a =? b.
+Definition hidden_eq (a b : Z) := (a =? b)%Z.
 Ltac all_rew :=
   repeat match goal with
-         | [ |- context [ ?A =? ?B]] =>
-           change (A =? B) with (hidden_eq A B)
+         | [ |- context [ (?A =? ?B)%Z]] =>
+           change (A =? B)%Z with (hidden_eq A B)
          end;
   repeat match goal with
          | [ |- context [ hidden_eq ?A ?B] ] =>
-           replace (hidden_eq A B) with (B =? A);
+           replace (hidden_eq A B) with (B =? A)%Z;
            [ | now rewrite Z.eqb_sym]
          end.
 
@@ -112,3 +112,11 @@ Ltac cvc4_no_check   := prop2bool; cvc4_bool_no_check; bool2prop.
 
 Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop).
 Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop).
+
+
+
+(* 
+   Local Variables:
+   coq-load-path: ((rec "." "SMTCoq"))
+   End: 
+*)
diff --git a/src/array/FArray.v b/src/array/FArray.v
index 8b1701f..1f8c6b4 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -11,7 +11,7 @@
 
 
 Require Import Bool OrderedType SMT_classes.
-Require Import ProofIrrelevance.
+Require Import ProofIrrelevance. (* TODO: REMOVE THIS AXIOM *)
 
 (** This file formalizes functional arrays with extensionality as specified in
     SMT-LIB 2. It gives realization to axioms that define the SMT-LIB theory of
@@ -474,7 +474,7 @@ Module Raw.
 
   (** * [mem] *)
 
-  Function mem (k : key) (s : farray) {struct s} : bool :=
+  Fixpoint mem (k : key) (s : farray) {struct s} : bool :=
     match s with
     | nil => false
     | (k',_) :: l =>
@@ -488,30 +488,31 @@ Module Raw.
   Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true.
   Proof.
     intros m Hm x; generalize Hm; clear Hm.
-    functional induction (mem x m);intros sorted belong1;trivial.
-
-    inversion belong1. inversion H.
-
-    absurd (In x ((k', _x) :: l));try assumption.
-    apply Sort_Inf_NotIn with _x;auto.
-
-    apply IHb.
-    elim (sort_inv sorted);auto.
-    elim (In_inv belong1);auto.
-    intro abs.
-    absurd (eq x k'); auto.
-    symmetry in abs.
-    apply lt_not_eq in abs; auto.
+    induction m as [ |[k' _x] l IHb]; intros sorted belong1.
+    - inversion belong1. inversion H.
+    - simpl. case_eq (compare x k'); trivial.
+      + intros _x0 e0.
+        absurd (In x ((k', _x) :: l));try assumption.
+        apply Sort_Inf_NotIn with _x;auto.
+      + intros _x0 e0.
+        apply IHb.
+        elim (sort_inv sorted);auto.
+        elim (In_inv belong1);auto.
+        intro abs.
+        absurd (eq x k'); auto.
+        symmetry in abs.
+        apply lt_not_eq in abs; auto.
   Qed.
 
   Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
   Proof.
     intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo.
-    functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail).
-    exists _x; auto.
-    induction IHb; auto.
-    exists x0; auto.
-    inversion_clear sorted; auto.
+    induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail).
+    revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail).
+    - exists _x; auto.
+    - induction IHb; auto.
+      + exists x0; auto.
+      + inversion_clear sorted; auto.
   Qed.
 
   Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m.
@@ -523,7 +524,7 @@ Module Raw.
 
   (** * [find] *)
 
-  Function find (k:key) (s: farray) {struct s} : option elt :=
+  Fixpoint find (k:key) (s: farray) {struct s} : option elt :=
     match s with
     | nil => None
     | (k',x)::s' =>
@@ -537,43 +538,40 @@ Module Raw.
   Lemma find_2 :  forall m x e, find x m = Some e -> MapsTo x e m.
   Proof.
     intros m x. unfold MapsTo.
-    functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto.
+    induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto).
+    case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto.
   Qed.
 
   Lemma find_1 :  forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
   Proof.
     intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo.
-    functional induction (find x m);simpl; subst; try clear H_eq_1.
-
-    inversion 2.
-
-    inversion_clear 2.
-    clear e1;compute in H0; destruct H0.
-    apply lt_not_eq in H; auto. now contradict H.
-
-    clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
-    (* order. *)
-    intros.
-    apply (lt_trans k') in _x; auto.
-    apply lt_not_eq in _x.
-    now contradict _x.
-
-    clear e1;inversion_clear 2.
-    compute in H0; destruct H0; intuition congruence.
-    generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
-    (* order. *)
-    intros.
-    apply lt_not_eq in H. now contradict H.
-
-    clear e1; do 2 inversion_clear 1; auto.
-    compute in H2; destruct H2.
-    (* order. *)
-    subst. apply lt_not_eq in _x. now contradict _x.
+    induction m as [ |[k' _x] l IHb];simpl; subst; try clear H_eq_1.
+    - inversion 2.
+    - case_eq (compare x k'); intros _x0 e1; subst.
+      + inversion_clear 2.
+        * clear e1;compute in H0; destruct H0.
+          apply lt_not_eq in H; auto. now contradict H.
+        * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
+          (* order. *)
+          intros.
+          apply (lt_trans k') in _x0; auto.
+          apply lt_not_eq in _x0.
+          now contradict _x0.
+      + clear e1;inversion_clear 2.
+        * compute in H0; destruct H0; intuition congruence.
+        * generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
+          (* order. *)
+          intros.
+          apply lt_not_eq in H. now contradict H.
+      + clear e1; do 2 inversion_clear 1; auto.
+        compute in H2; destruct H2.
+        (* order. *)
+        subst. apply lt_not_eq in _x0. now contradict _x0.
   Qed.
 
   (** * [add] *)
 
-  Function add (k : key) (x : elt) (s : farray) {struct s} : farray :=
+  Fixpoint add (k : key) (x : elt) (s : farray) {struct s} : farray :=
     match s with
     | nil => (k,x) :: nil
     | (k',y) :: l =>
@@ -588,7 +586,7 @@ Module Raw.
   Proof.
     intros m x y e; generalize y; clear y.
     unfold MapsTo.
-    functional induction (add x e m);simpl;auto.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto.
   Qed.
 
   Lemma add_2 : forall m x y e e',
@@ -596,7 +594,7 @@ Module Raw.
   Proof.
     intros m x  y e e'.
     generalize y e; clear y e; unfold MapsTo.
-    functional induction (add x e' m) ;simpl;auto;  clear e0.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto;  clear e0.
     subst;auto.
 
     intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
@@ -611,7 +609,7 @@ Module Raw.
       ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
   Proof.
     intros m x y e e'. generalize y e; clear y e; unfold MapsTo.
-    functional induction (add x e' m);simpl; intros.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];simpl; intros.
     apply (In_inv_3 H0); compute; auto.
     apply (In_inv_3 H0); compute; auto.
     constructor 2; apply (In_inv_3 H0); compute; auto.
@@ -644,7 +642,7 @@ Module Raw.
 
   (** * [remove] *)
 
-  Function remove (k : key) (s : farray) {struct s} : farray :=
+  Fixpoint remove (k : key) (s : farray) {struct s} : farray :=
     match s with
     | nil => nil
     | (k',x) :: l =>
@@ -658,7 +656,7 @@ Module Raw.
   Lemma remove_1 : forall m (Hm:Sort m) x y, eq x y -> ~ In y (remove x m).
   Proof.
     intros m Hm x y; generalize Hm; clear Hm.
-    functional induction (remove x m);simpl;intros;subst.
+    induction m as [ |[k' x0] l IHb]; simpl;intros; [ |case_eq (compare x k'); intros _x e0];simpl;intros;subst.
 
     red; inversion 1; inversion H0.
 
@@ -685,7 +683,7 @@ Module Raw.
       ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
   Proof.
     intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
-    functional induction (remove x m);subst;auto;
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
@@ -701,7 +699,7 @@ Module Raw.
       MapsTo y e (remove x m) -> MapsTo y e m.
   Proof.
     intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
-    functional induction (remove x m);subst;auto.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto.
     inversion_clear 1; inversion_clear 1; auto.
   Qed.
 
@@ -709,7 +707,7 @@ Module Raw.
       ~ eq x y -> In y m -> In y (remove x m).
   Proof.
     intros m Hm x y; generalize Hm; clear Hm.
-    functional induction (remove x m);subst;auto;
+    induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
@@ -719,7 +717,7 @@ Module Raw.
     inversion H2.
     unfold eqk in H3. simpl in H3. subst. now contradict H0.
     apply In_alt.
-    exists x1. auto.
+    exists x. auto.
     apply lt_not_eq in _x.
     intros.
     inversion_clear Hm.
@@ -750,7 +748,7 @@ Module Raw.
     apply remove_4_aux; auto.
     revert H.
     generalize Hm; clear Hm.
-    functional induction (remove x m);subst;auto;
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
@@ -761,16 +759,16 @@ Module Raw.
     exists e.
     apply InA_cons_tl. auto.
     intros.
-    apply lt_not_eq in _x.
+    apply lt_not_eq in _x0.
     inversion_clear Hm.
     apply In_inv in H0.
     destruct H0.
     (* destruct (eq_dec k' y). *)
-    exists x0.
+    exists _x.
     apply InA_cons_hd. split; simpl; auto.
-    specialize (IHf H1 H H0).
-    inversion IHf.
-    exists x1.
+    specialize (IHb H1 H H0).
+    inversion IHb.
+    exists x0.
     apply InA_cons_tl. auto.
   Qed.
 
@@ -828,7 +826,7 @@ Module Raw.
 
   (** * [fold] *)
 
-  Function fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} :  A :=
+  Fixpoint fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} :  A :=
     match m with
     | nil => acc
     | (k,e)::m' => fold f m' (f k e acc)
@@ -837,12 +835,12 @@ Module Raw.
   Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A),
       fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
   Proof.
-    intros; functional induction (fold f m i); auto.
+    intros; revert i; induction m as [ |[k e]]; simpl; auto.
   Qed.
 
   (** * [equal] *)
 
-  Function equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool :=
+  Fixpoint equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool :=
     match m, m' with
     | nil, nil => true
     | (x,e)::l, (x',e')::l' =>
@@ -861,121 +859,112 @@ Module Raw.
       Equivb cmp m m' -> equal cmp m m' = true.
   Proof.
     intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
-    functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
+    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto; unfold Equivb; intuition; subst.
+    - destruct (H0 x') as [_ H3].
+      assert (H2: In x' nil).
+      {
+        apply H3. exists e'. now constructor.
+      }
+      elim H2. intros x Hx. inversion Hx.
+    - destruct (H0 x) as [H3 _].
+      assert (H2: In x nil).
+      {
+        apply H3. exists e. now constructor.
+      }
+      elim H2. intros x0 Hx0. inversion Hx0.
+    - case_eq (compare x x'); simpl; subst;auto; unfold Equivb;
       intuition; subst.
-    match goal with H: compare _ _ = _ |- _ => clear H end.
-    assert (cmp_e_e':cmp e e' = true).
-    apply H1 with x; auto.
-    rewrite cmp_e_e'; simpl.
-    apply IHb; auto.
-    inversion_clear Hm; auto.
-    inversion_clear Hm'; auto.
-    unfold Equivb; intuition.
-    destruct (H0 k).
-    assert (In k ((x,e) ::l)).
-    destruct H as (e'', hyp); exists e''; auto.
-    destruct (In_inv (H2 H4)); auto.
-    inversion_clear Hm.
-    elim (Sort_Inf_NotIn H6 H7).
-    destruct H as (e'', hyp); exists e''; auto.
-    apply MapsTo_eq with k; auto.
-    destruct (H0 k).
-    assert (In k ((x,e') ::l')).
-    destruct H as (e'', hyp); exists e''; auto.
-    destruct (In_inv (H3 H4)); auto.
-    subst.
-    inversion_clear Hm'.
-    now elim (Sort_Inf_NotIn H5 H6).
-    apply H1 with k; destruct (eq_dec x k); auto.
-
-
-    destruct (compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y.
-    destruct (H0 x).
-    assert (In x ((x',e')::l')).
-    apply H; auto.
-    exists e; auto.
-    destruct (In_inv H3).
-    (* order. *)
-    apply lt_not_eq in Hlt; now contradict Hlt.
-    inversion_clear Hm'.
-    assert (Inf (x,e) l').
-    apply Inf_lt with (x',e'); auto.
-    elim (Sort_Inf_NotIn H5 H7 H4).
-
-    destruct (H0 x').
-    assert (In x' ((x,e)::l)).
-    apply H2; auto.
-    exists e'; auto.
-    destruct (In_inv H3).
-    (* order. *)
-    subst; apply lt_not_eq in Hlt; now contradict Hlt.
-    inversion_clear Hm.
-    assert (Inf (x',e') l).
-    apply Inf_lt with (x,e); auto.
-    elim (Sort_Inf_NotIn H5 H7 H4).
-
-    destruct m;
-      destruct m';try contradiction.
-
-    clear H1;destruct p as (k,e).
-    destruct (H0 k).
-    destruct H1.
-    exists e; auto.
-    inversion H1.
-
-    destruct p as (x,e).
-    destruct (H0 x).
-    destruct H.
-    exists e; auto.
-    inversion H.
-
-    destruct p;destruct p0;contradiction.
+      + destruct (H0 x).
+        assert (In x ((x',e')::l')).
+        apply H2; auto.
+        exists e; auto.
+        destruct (In_inv H4).
+        (* order. *)
+        clear H. apply lt_not_eq in l0; now contradict l0.
+        inversion_clear Hm'.
+        assert (Inf (x,e) l').
+        apply Inf_lt with (x',e'); auto.
+        elim (Sort_Inf_NotIn H6 H8 H5).
+      + match goal with H: compare _ _ = _ |- _ => clear H end.
+        assert (cmp_e_e':cmp e e' = true).
+        apply H1 with x'; auto.
+        rewrite cmp_e_e'; simpl.
+        apply IHl; auto.
+        inversion_clear Hm; auto.
+        inversion_clear Hm'; auto.
+        unfold Equivb; intuition.
+        destruct (H0 k).
+        assert (In k ((x',e) ::l)).
+        destruct H as (e'', hyp); exists e''; auto.
+        destruct (In_inv (H2 H4)); auto.
+        inversion_clear Hm.
+        elim (Sort_Inf_NotIn H6 H7).
+        destruct H as (e'', hyp); exists e''; auto.
+        apply MapsTo_eq with k; auto.
+        destruct (H0 k).
+        assert (In k ((x',e') ::l')).
+        destruct H as (e'', hyp); exists e''; auto.
+        destruct (In_inv (H3 H4)); auto.
+        subst.
+        inversion_clear Hm'.
+        now elim (Sort_Inf_NotIn H5 H6).
+        apply H1 with k; destruct (eq_dec x' k); auto.
+      + destruct (H0 x').
+        assert (In x' ((x,e)::l)).
+        apply H3; auto.
+        exists e'; auto.
+        destruct (In_inv H4).
+        (* order. *)
+        clear H; subst; apply lt_not_eq in l0; now contradict l0.
+        inversion_clear Hm.
+        assert (Inf (x',e') l).
+        apply Inf_lt with (x,e); auto.
+        elim (Sort_Inf_NotIn H6 H8 H5).
   Qed.
 
   Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp,
       equal cmp m m' = true -> Equivb cmp m m'.
   Proof.
     intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
-    functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
+    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto; unfold Equivb;
       intuition; try discriminate; subst;
         try match goal with H: compare _ _ = _ |- _ => clear H end.
-
-    inversion H0.
-
-    inversion_clear Hm;inversion_clear Hm'.
-    destruct (andb_prop _ _ H); clear H.
-    destruct (IHb H1 H3 H6).
-    destruct (In_inv H0).
-    exists e'; constructor; split; trivial; apply eq_trans with x; auto.
-    destruct (H k).
-    destruct (H9 H8) as (e'',hyp).
-    exists e''; auto.
-
-    inversion_clear Hm;inversion_clear Hm'.
-    destruct (andb_prop _ _ H); clear H.
-    destruct (IHb H1 H3 H6).
-    destruct (In_inv H0).
-    exists e; constructor; split; trivial; apply eq_trans with x'; auto.
-    destruct (H k).
-    destruct (H10 H8) as (e'',hyp).
-    exists e''; auto.
-
-    inversion_clear Hm;inversion_clear Hm'.
-    destruct (andb_prop _ _ H); clear H.
-    destruct (IHb H2 H4 H7).
-    inversion_clear H0.
-    destruct H9; simpl in *; subst.
-    inversion_clear H1.
-    destruct H0; simpl in *; subst; auto.
-    elim (Sort_Inf_NotIn H4 H5).
-    exists e'0; apply MapsTo_eq with x; auto.
+    - inversion H0.
+    - revert H; case_eq (compare x x'); intros _x _ H; try inversion H.
+      inversion_clear Hm;inversion_clear Hm'.
+      destruct (andb_prop _ _ H); clear H.
+      destruct (IHl _ H1 H4 H7).
+      destruct (In_inv H0).
+      exists e'; constructor; split; trivial; apply eq_trans with x; auto.
+      destruct (H k).
+      destruct (H10 H9) as (e'',hyp).
+      exists e''; auto.
+    - revert H; case_eq (compare x x'); intros _x _ H; try inversion H.
+      inversion_clear Hm;inversion_clear Hm'.
+      destruct (andb_prop _ _ H); clear H.
+      destruct (IHl _ H1 H4 H7).
+      destruct (In_inv H0).
+      exists e; constructor; split; trivial; apply eq_trans with x'; auto.
+      destruct (H k).
+      destruct (H11 H9) as (e'',hyp).
+      exists e''; auto.
+    - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H].
+      inversion_clear Hm;inversion_clear Hm'.
+      destruct (andb_prop _ _ H); clear H.
+      destruct (IHl _ H2 H4 H7).
+      inversion_clear H0.
+      + destruct H9; simpl in *; subst.
+        inversion_clear H1.
+        * destruct H0; simpl in *; subst; auto.
+        * elim (Sort_Inf_NotIn H4 H5).
+          exists e'0; apply MapsTo_eq with x'; auto.
       (* order. *)
-    inversion_clear H1.
-    destruct H0; simpl in *; subst; auto.
-    elim (Sort_Inf_NotIn H2 H3).
-    exists e0; apply MapsTo_eq with x; auto.
-    (* order. *)
-    apply H8 with k; auto.
+      + inversion_clear H1.
+        * destruct H0; simpl in *; subst; auto.
+          elim (Sort_Inf_NotIn H2 H3).
+          exists e0; apply MapsTo_eq with x'; auto.
+        (* order. *)
+        * apply H8 with k; auto.
   Qed.
 
   (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *)
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 48befd6..a53970b 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import List Bool NArith Psatz Int63 Nnat.
+Require Import List Bool NArith Psatz Int63 Nnat ZArith.
 Require Import Misc.
 Import ListNotations.
 Local Open Scope list_scope.
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 81e0a30..84df9bd 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -12,11 +12,9 @@
 
 (** A small checker for bit-vectors bit-blasting *)
 
-(*Add Rec LoadPath "." as SMTCoq.*)
-
 Require Structures.
 
-Require Import Int63 Int63Properties PArray SMT_classes.
+Require Import Int63 Int63Properties PArray SMT_classes ZArith.
 
 Require Import Misc State SMT_terms BVList Psatz.
 Require Import Bool List BoolEq NZParity Nnat.
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index 73f9f97..ec18c15 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import PArray List Bool.
+Require Import PArray List Bool ZArith.
 Require Import Misc State SMT_terms BVList.
 
 Import Form.
diff --git a/src/configure.sh b/src/configure.sh
index 52f21b3..cc2a1ca 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -21,7 +21,9 @@ if [ $@ -a $@ = -native ]; then
     cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4
     cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v
 else
+    cp ${pre}versions/standard/Make ${pre}Make
     cp ${pre}versions/standard/Makefile ${pre}Makefile
+    cp ${pre}versions/standard/Makefile.conf ${pre}Makefile.conf
     cp ${pre}versions/standard/g_smtcoq_standard.ml4 ${pre}g_smtcoq.ml4
     cp ${pre}versions/standard/smtcoq_plugin_standard.mlpack ${pre}smtcoq_plugin.mlpack
     cp ${pre}versions/standard/Int63/Int63_standard.v ${pre}versions/standard/Int63/Int63.v
diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml
index 29a4afc..454bc0a 100644
--- a/src/lfsc/ast.ml
+++ b/src/lfsc/ast.ml
@@ -83,12 +83,12 @@ let value t = (deref t).value
 let ttype t = deref (deref t).ttype
 
 
-let rec name c = match value c with
+let name c = match value c with
   | Const {sname=Name n} -> Some n
   | _ -> None
 
 
-let rec app_name r = match value r with
+let app_name r = match value r with
   | App ({value=Const{sname=Name n}}, args) -> Some (n, args)
   | _ -> None
 
@@ -298,36 +298,36 @@ end
 
 
 
-let rec holes_address acc t = match t.value with
-  | Hole i -> (i, t) :: acc
-  | Type | Kind |  Mpz | Mpq | Int _ | Rat _  -> acc
-  | SideCond (name, args, exp, t) -> acc
-  | Const _ -> acc
-  | App (f, args) ->
-    List.fold_left holes_address acc args 
-  | Pi (s, x) -> holes_address acc x
-  | Lambda (s, x) -> holes_address acc x
-  | Ptr t -> holes_address acc t
-
-let holes_address = holes_address []
-
-
-let check_holes_integrity where h1 h2 =
-  List.iter (fun (i, a) ->
-      List.iter (fun (j, b) ->
-          if j = i && a != b then
-            (
-              eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i
-                (address_of a) (address_of b);
-              (* eprintf "\n%s: Hole _%d has changed\n@." where i; *)
-              assert false)
-        ) h2
-    ) h1
-
-let check_term_integrity where t = 
-  let h = holes_address t in
-  check_holes_integrity (where ^ "term has != _") h h
-    
+(* let rec holes_address acc t = match t.value with
+ *   | Hole i -> (i, t) :: acc
+ *   | Type | Kind |  Mpz | Mpq | Int _ | Rat _  -> acc
+ *   | SideCond (name, args, exp, t) -> acc
+ *   | Const _ -> acc
+ *   | App (f, args) ->
+ *     List.fold_left holes_address acc args
+ *   | Pi (s, x) -> holes_address acc x
+ *   | Lambda (s, x) -> holes_address acc x
+ *   | Ptr t -> holes_address acc t *)
+
+(* let holes_address = holes_address [] *)
+
+
+(* let check_holes_integrity where h1 h2 =
+ *   List.iter (fun (i, a) ->
+ *       List.iter (fun (j, b) ->
+ *           if j = i && a != b then
+ *             (
+ *               eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i
+ *                 (address_of a) (address_of b);
+ *               (\* eprintf "\n%s: Hole _%d has changed\n@." where i; *\)
+ *               assert false)
+ *         ) h2
+ *     ) h1 *)
+
+(* let check_term_integrity where t =
+ *   let h = holes_address t in
+ *   check_holes_integrity (where ^ "term has != _") h h *)
+
 
 
 let eq_name s1 s2 = match s1, s2 with
@@ -471,10 +471,10 @@ module MSym = Map.Make (struct
 
 let empty_subst = MSym.empty
 
-let fresh_alpha =
-  let cpt = ref 0 in
-  fun ty -> incr cpt;
-    mk_symbol ("'a"^string_of_int !cpt) ty
+(* let fresh_alpha =
+ *   let cpt = ref 0 in
+ *   fun ty -> incr cpt;
+ *     mk_symbol ("'a"^string_of_int !cpt) ty *)
 
 
 let get_t ?(gen=true) sigma s =
@@ -834,20 +834,20 @@ let rec hole_nbs acc t = match value t with
   | _ -> acc
 
 
-let rec min_hole acc t = match value t with
-  | Hole nb ->
-    (match acc with Some n when nb < n -> Some nb  | None -> Some nb | _ -> acc)
-  | App (f, args) -> List.fold_left min_hole (min_hole acc f) args 
-  | Pi (s, x) | Lambda (s, x) -> min_hole acc x
-  | Ptr t -> min_hole acc t
-  | _ -> acc
+(* let rec min_hole acc t = match value t with
+ *   | Hole nb ->
+ *     (match acc with Some n when nb < n -> Some nb  | None -> Some nb | _ -> acc)
+ *   | App (f, args) -> List.fold_left min_hole (min_hole acc f) args
+ *   | Pi (s, x) | Lambda (s, x) -> min_hole acc x
+ *   | Ptr t -> min_hole acc t
+ *   | _ -> acc *)
 
 
-let compare_int_opt m1 m2 = match m1, m2 with
-  | None, None -> 0
-  | Some _, None -> -1
-  | None, Some _ -> 1
-  | Some n1, Some n2 -> compare n1 n2
+(* let compare_int_opt m1 m2 = match m1, m2 with
+ *   | None, None -> 0
+ *   | Some _, None -> -1
+ *   | None, Some _ -> 1
+ *   | Some n1, Some n2 -> compare n1 n2 *)
 
 
 let compare_sc_checks (_, args1, exp1) (_, args2, exp2) =
diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml
index 7d0151b..86899df 100644
--- a/src/lfsc/builtin.ml
+++ b/src/lfsc/builtin.ml
@@ -11,7 +11,6 @@
 
 
 open Ast
-open Format
 
 
 module H = struct
@@ -90,7 +89,7 @@ module H = struct
 
   let var_bv = Hstring.make "var_bv"
 
-  let a_var_bv = Hstring.make "a_var_bv"
+  (* let a_var_bv = Hstring.make "a_var_bv" *)
   let a_bv = Hstring.make "a_bv"
   let a_int = Hstring.make "a_int"
 
@@ -98,7 +97,7 @@ module H = struct
   let bitof = Hstring.make "bitof"
   let bblast_term = Hstring.make "bblast_term"
 
-  let eq = Hstring.make "="
+  (* let eq = Hstring.make "=" *)
   let bvand = Hstring.make "bvand"
   let bvor = Hstring.make "bvor"
   let bvxor = Hstring.make "bvxor"
@@ -163,7 +162,7 @@ module H = struct
   let tfalse = Hstring.make "false"
   let a_var_bv = Hstring.make "a_var_bv"
   let eq = Hstring.make "="
-  let trust_f = Hstring.make "trust_f"
+  (* let trust_f = Hstring.make "trust_f" *)
   let ext = Hstring.make "ext"
   let decl_atom = Hstring.make "decl_atom"
   let asf = Hstring.make "asf"
@@ -179,7 +178,7 @@ module H = struct
   let or_elim_1 = Hstring.make "or_elim_1"
   let or_elim_2 = Hstring.make "or_elim_2"
   let iff_elim_1 = Hstring.make "iff_elim_1"
-  let iff_elim_2 = Hstring.make "iff_elim_2"
+  (* let iff_elim_2 = Hstring.make "iff_elim_2" *)
   let impl_elim = Hstring.make "impl_elim"
   let not_and_elim = Hstring.make "not_and_elim"
   let xor_elim_1 = Hstring.make "xor_elim_1"
@@ -232,8 +231,8 @@ module H = struct
   let bv_bbl_bvneg = Hstring.make "bv_bbl_bvneg"
   let bv_bbl_bvadd = Hstring.make "bv_bbl_bvadd"
   let bv_bbl_bvmul = Hstring.make "bv_bbl_bvmul"
-  let bv_bbl_bvult = Hstring.make "bv_bbl_bvult"
-  let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt"
+  (* let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" *)
+  (* let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" *)
   let bv_bbl_concat = Hstring.make "bv_bbl_concat"
   let bv_bbl_extract = Hstring.make "bv_bbl_extract"
   let bv_bbl_zero_extend = Hstring.make "bv_bbl_zero_extend"
@@ -1172,7 +1171,7 @@ let rec bblast_bvult x y n =
   | _ -> failwith "bblast_bvult"
 
 
-let rec bblast_bvslt x y n =
+let bblast_bvslt x y n =
   match value x with
   | App (ff, [xi; x']) when term_equal ff bbltc_s ->
     (match value y with
diff --git a/src/lfsc/converter.ml b/src/lfsc/converter.ml
index d586e37..2dfbed3 100644
--- a/src/lfsc/converter.ml
+++ b/src/lfsc/converter.ml
@@ -874,19 +874,19 @@ module Make (T : Translator_sig.S) = struct
       | _ -> raise Not_found
              
 
-  let rec reso_of_QR acc qr = match app_name qr with
-    | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
-      reso_of_QR (reso_of_QR acc u1) u2
-    | _ -> clause_qr qr :: acc
+  (* let rec reso_of_QR acc qr = match app_name qr with
+   *   | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
+   *     reso_of_QR (reso_of_QR acc u1) u2
+   *   | _ -> clause_qr qr :: acc *)
 
   (** Returns clauses used in a linear resolution chain *)
-  let reso_of_QR qr = reso_of_QR [] qr |> List.rev
+  (* let reso_of_QR qr = reso_of_QR [] qr |> List.rev *)
 
 
-  let rec reso_of_QR qr = match app_name qr with
-    | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
-      reso_of_QR u1 @ reso_of_QR u2
-    | _ -> [clause_qr qr]
+  (* let rec reso_of_QR qr = match app_name qr with
+   *   | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
+   *     reso_of_QR u1 @ reso_of_QR u2
+   *   | _ -> [clause_qr qr] *)
 
   let rec reso_of_QR depth acc qr = match app_name qr with
     | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
@@ -963,7 +963,7 @@ module Make (T : Translator_sig.S) = struct
       | None -> assert false
 
 
-  let rec bb_lem env p =
+  let bb_lem env p =
     let env, p = bb_trim_intro_unit env p in
     let id = bb_lem_res None p in
     { env with clauses = id :: env.clauses }
diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
index 0f9fd8d..a11139d 100644
--- a/src/lfsc/lfsc.ml
+++ b/src/lfsc/lfsc.ml
@@ -11,13 +11,9 @@
 
 
 open Format
-open Entries
-open Declare
-open Decl_kinds
 
 open SmtMisc
 open CoqTerms
-open SmtForm
 open SmtCertif
 open SmtTrace
 open SmtAtom
@@ -163,8 +159,8 @@ let checker_debug fsmt fproof =
 let theorem name fsmt fproof =
   SmtCommands.theorem name (import_all fsmt fproof)
 
-let checker fsmt fproof =
-  SmtCommands.checker (import_all fsmt fproof)
+(* let checker fsmt fproof =
+ *   SmtCommands.checker (import_all fsmt fproof) *)
 
 (* Same but print runtime *)
 let checker fsmt fproof =
diff --git a/src/lfsc/lfscLexer.mll b/src/lfsc/lfscLexer.mll
index 3e8d5f9..242df00 100644
--- a/src/lfsc/lfscLexer.mll
+++ b/src/lfsc/lfscLexer.mll
@@ -245,7 +245,7 @@ and scan_string buf start = parse
       {
         let ofs = lexbuf.lex_start_pos in
         let len = lexbuf.lex_curr_pos - ofs in
-        Quoted_string_buffer.add_substring buf lexbuf.lex_buffer ofs len;
+        Quoted_string_buffer.add_substring buf (Bytes.to_string lexbuf.lex_buffer) ofs len;
         Quoted_string_buffer.add_lexeme buf lexbuf;
         scan_string buf start lexbuf
       }
diff --git a/src/lfsc/lfscParser.mly b/src/lfsc/lfscParser.mly
index 26de090..3d6749f 100644
--- a/src/lfsc/lfscParser.mly
+++ b/src/lfsc/lfscParser.mly
@@ -16,7 +16,6 @@
 open Ast
 open Lexing
 open Format
-open Builtin
 
 let parse_failure what =
   let pos = Parsing.symbol_start_pos () in
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index 0395244..f520ba7 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -12,8 +12,6 @@
 
 open SmtAtom
 open SmtForm
-open SmtCertif
-open SmtTrace
 open VeritSyntax
 open Ast
 open Builtin
@@ -42,7 +40,7 @@ module HT = struct
   let add h k v = h := M.add k v !h
   let find h k = M.find k !h
   let clear h = h := M.empty
-  let iter f h = M.iter f !h
+  (* let iter f h = M.iter f !h *)
 end
 
 
@@ -499,8 +497,8 @@ let register_clause_id cl id =
   Hashtbl.add ids_clauses id cl
 
 
-let register_termclause_id t id =
-  register_clause_id (to_clause t) id
+(* let register_termclause_id t id =
+ *   register_clause_id (to_clause t) id *)
 
 
 let new_clause_id ?(reuse=true) cl =
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index cafac1b..8c5a597 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import Bool List Int63 PArray.
+Require Import Bool List Int63 PArray ZArith.
 Require Import Misc State SMT_terms Euf.
 
 Require Import RingMicromega ZMicromega Tauto Psatz.
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index adeed4e..d8ed560 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -11,11 +11,6 @@
 
 
 (*** Linking SMT Terms to Micromega Terms ***)
-open Term
-open Coqlib
-open Declare
-open Decl_kinds
-open Entries
 open Util
 open Structures.Micromega_plugin_Micromega
 open Structures.Micromega_plugin_Coq_micromega
@@ -114,7 +109,7 @@ let smt_binop_to_micromega_formula tbl op ha hb =
   let rhs = smt_Atom_to_micromega_pExpr tbl hb in
   {flhs = lhs; fop = op; frhs = rhs }
 
-let rec smt_Atom_to_micromega_formula tbl ha =
+let smt_Atom_to_micromega_formula tbl ha =
   match Atom.atom ha with
     | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb
     | _ -> Structures.error
@@ -122,7 +117,7 @@ let rec smt_Atom_to_micromega_formula tbl ha =
 
 (* specialized fold *)
 
-let default_constr = mkInt 0
+let default_constr = Structures.econstr_of_constr (mkInt 0)
 let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0
 (* morphism for general formulas *)
 
diff --git a/src/lia/lia.mli b/src/lia/lia.mli
index 93361f2..9d4ee6b 100644
--- a/src/lia/lia.mli
+++ b/src/lia/lia.mli
@@ -12,7 +12,7 @@
 
 val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive
 val z_of_int : int -> Structures.Micromega_plugin_Micromega.z
-type my_tbl = { tbl : (SmtAtom.hatom, int) Hashtbl.t; mutable count : int; }
+type my_tbl
 val get_atom_var : my_tbl -> SmtAtom.hatom -> int
 val create_tbl : int -> my_tbl
 val smt_Atom_to_micromega_pos :
@@ -36,8 +36,6 @@ val smt_Atom_to_micromega_formula :
   SmtAtom.hatom ->
   Structures.Micromega_plugin_Micromega.z
   Structures.Micromega_plugin_Micromega.formula
-val default_constr : Term.constr
-val default_tag : Structures.Micromega_plugin_Mutils.Tag.t
 val binop_array :
   ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c
 val smt_Form_to_coq_micromega_formula :
diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
index 7317b60..65dc3e3 100644
--- a/src/smtlib2/smtlib2_ast.ml
+++ b/src/smtlib2/smtlib2_ast.ml
@@ -16,8 +16,6 @@
 (**************************************************************************)
 
 
-open Smtlib2_util
-
 type loc = Lexing.position * Lexing.position
 
 type specconstant =
@@ -191,65 +189,65 @@ let loc_of e = loc_commands e;;
 
 
 
-let print_specconstant fmt = function
-  | SpecConstsDec (_, s)
-  | SpecConstNum (_, s)
-  | SpecConstString (_, s)
-  | SpecConstsHex (_, s)
-  | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s
-
-
-let print_symbol fmt = function
-  | Symbol (_, s)
-  | SymbolWithOr (_, s) -> Format.pp_print_string fmt s
-
-
-let print_identifier fmt = function
-  | IdSymbol (_, s) -> print_symbol fmt s
-  | IdUnderscoreSymNum (_, s, (_, l)) ->
-    Format.fprintf fmt "(_ %a" print_symbol s;
-    List.iter (Format.fprintf fmt " %s") l;
-    Format.fprintf fmt ")"  
-    
-let rec print_sort fmt = function
-  | SortIdentifier (_, i) -> print_identifier fmt i
-  | SortIdSortMulti (_, i, (_, ls)) ->
-    Format.fprintf fmt "(%a" print_identifier i;
-    List.iter (Format.fprintf fmt " %a" print_sort) ls;
-    Format.fprintf fmt ")"  
-
-let print_qualidentifier fmt = function
-  | QualIdentifierId (_, i) -> print_identifier fmt i
-  | QualIdentifierAs (_, i, s) ->
-    Format.fprintf fmt "(%a as %a)"
-      print_identifier i print_sort s 
-
-let print_sortedvar fmt = function
-  | SortedVarSymSort (_, v, s) ->
-    Format.fprintf fmt "(%a %a)" print_symbol v print_sort s
-
-let rec print_varbinding fmt = function
-  | VarBindingSymTerm (_, s, t) ->
-    Format.fprintf fmt "(%a %a)" print_symbol s print_term t
-
-and print_term fmt = function
-  | TermSpecConst (_, c) -> print_specconstant fmt c
-  | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
-  | TermQualIdTerm (_, i, (_, tl)) ->
-    Format.fprintf fmt "(%a" print_qualidentifier i;
-    List.iter (Format.fprintf fmt " %a" print_term) tl;
-    Format.fprintf fmt ")"  
-  | TermLetTerm (_, (_, vb), t) ->
-    Format.fprintf fmt "(let (";
-    List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermForAllTerm (_, (_, sv), t) ->
-    Format.fprintf fmt "(forall (";
-    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermExistsTerm (_, (_, sv), t) ->
-    Format.fprintf fmt "(exists (";
-    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermExclimationPt (_, t, _) -> print_term fmt t
+(* let print_specconstant fmt = function
+ *   | SpecConstsDec (_, s)
+ *   | SpecConstNum (_, s)
+ *   | SpecConstString (_, s)
+ *   | SpecConstsHex (_, s)
+ *   | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_symbol fmt = function
+ *   | Symbol (_, s)
+ *   | SymbolWithOr (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_identifier fmt = function
+ *   | IdSymbol (_, s) -> print_symbol fmt s
+ *   | IdUnderscoreSymNum (_, s, (_, l)) ->
+ *     Format.fprintf fmt "(_ %a" print_symbol s;
+ *     List.iter (Format.fprintf fmt " %s") l;
+ *     Format.fprintf fmt ")" *)
+
+(* let rec print_sort fmt = function
+ *   | SortIdentifier (_, i) -> print_identifier fmt i
+ *   | SortIdSortMulti (_, i, (_, ls)) ->
+ *     Format.fprintf fmt "(%a" print_identifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_sort) ls;
+ *     Format.fprintf fmt ")" *)
+
+(* let print_qualidentifier fmt = function
+ *   | QualIdentifierId (_, i) -> print_identifier fmt i
+ *   | QualIdentifierAs (_, i, s) ->
+ *     Format.fprintf fmt "(%a as %a)"
+ *       print_identifier i print_sort s *)
+
+(* let print_sortedvar fmt = function
+ *   | SortedVarSymSort (_, v, s) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol v print_sort s *)
+
+(* let rec print_varbinding fmt = function
+ *   | VarBindingSymTerm (_, s, t) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol s print_term t *)
+
+(* and print_term fmt = function
+ *   | TermSpecConst (_, c) -> print_specconstant fmt c
+ *   | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
+ *   | TermQualIdTerm (_, i, (_, tl)) ->
+ *     Format.fprintf fmt "(%a" print_qualidentifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_term) tl;
+ *     Format.fprintf fmt ")"
+ *   | TermLetTerm (_, (_, vb), t) ->
+ *     Format.fprintf fmt "(let (";
+ *     List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermForAllTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(forall (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExistsTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(exists (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExclimationPt (_, t, _) -> print_term fmt t *)
 
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 692294d..203077b 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -50,7 +50,7 @@ let string_type s =
 let sort_of_string s = string_type s
 
 
-let sort_of_symbol s = sort_of_string (string_of_symbol s)
+(* let sort_of_symbol s = sort_of_string (string_of_symbol s) *)
 
 
 let rec bigint_binary_size acc i size =
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
index 40f73c7..dabd99b 100644
--- a/src/smtlib2/smtlib2_genConstr.mli
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -10,6 +10,7 @@
 (**************************************************************************)
 
 
+val pp_symbol : Smtlib2_ast.symbol -> string
 val parse_smt2bv : string -> bool list
 val bigint_bv : Big_int.big_int -> int -> string
 val import_smtlib2 :
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
index 3ee8229..8ae7202 100644
--- a/src/smtlib2/smtlib2_solver.ml
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -82,7 +82,7 @@ let read_success s =
   | r -> error s r
 
 
-let no_response _ = ()
+(* let no_response _ = () *)
 
 
 let read_check_result s = 
diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v
index cc34522..6d66a43 100644
--- a/src/spl/Syntactic.v
+++ b/src/spl/Syntactic.v
@@ -11,7 +11,7 @@
 
 
 (*** Spl -- a small checker for simplifications ***)
-Require Import List PArray Bool Int63 ZMicromega.
+Require Import List PArray Bool Int63 ZMicromega ZArith.
 Require Import Misc State SMT_terms BVList.
 Require Lia.
 
@@ -214,7 +214,7 @@ Section CheckAtom.
     end.
 
   (* TODO : move this *)
-  Lemma Zge_is_ge_bool : forall x y, (x >= y) <-> (Zge_bool x y = true).
+  Lemma Zge_is_ge_bool : forall x y, (x >= y)%Z <-> (Zge_bool x y = true).
   Proof.
     intros x y;assert (W:=Zge_cases x y);destruct (Zge_bool x y).
     split;auto.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 76f213b..895d217 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -12,8 +12,9 @@
 
 open Coqlib
 
-let gen_constant modules constant =
-  lazy (gen_constant_in_modules "SMT" modules constant)
+
+let gen_constant = Structures.gen_constant
+
 
 (* Int63 *)
 let cint = Structures.cint
@@ -65,7 +66,7 @@ let cleb = gen_constant z_modules "leb"
 let cgeb = gen_constant z_modules "geb"
 let cgtb = gen_constant z_modules "gtb"
 let ceqbZ = gen_constant z_modules "eqb"
-let cZeqbsym = gen_constant z_modules "eqb_sym"
+(* let cZeqbsym = gen_constant z_modules "eqb_sym" *)
 
 (* Booleans *)
 let bool_modules = [["Coq";"Bool";"Bool"]]
@@ -100,12 +101,12 @@ let cprod = gen_constant init_modules "prod"
 
 (* Dependent pairs *)
 let csigT = gen_constant init_modules "sigT"
-let cprojT1 = gen_constant init_modules "projT1"
-let cprojT2 = gen_constant init_modules "projT2"
-let cprojT3 = gen_constant init_modules "projT3"
+(* let cprojT1 = gen_constant init_modules "projT1" *)
+(* let cprojT2 = gen_constant init_modules "projT2" *)
+(* let cprojT3 = gen_constant init_modules "projT3" *)
 
-let csigT2 = gen_constant init_modules "sigT2"
-let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2"
+(* let csigT2 = gen_constant init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *)
 
 (* Logical Operators *)
 let cnot = gen_constant init_modules "not"
@@ -118,7 +119,7 @@ let cand = gen_constant init_modules "and"
 let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
 let cbitvector = gen_constant bv_modules "bitvector"
 let cof_bits = gen_constant bv_modules "of_bits"
-let c_of_bits = gen_constant bv_modules "_of_bits"
+(* let c_of_bits = gen_constant bv_modules "_of_bits" *)
 let cbitOf = gen_constant bv_modules "bitOf"
 let cbv_eq = gen_constant bv_modules "bv_eq"
 let cbv_not = gen_constant bv_modules "bv_not"
@@ -147,8 +148,8 @@ let cdiff = gen_constant array_modules "diff"
 let cequalarray = gen_constant array_modules "FArray.equal"
 
 (* OrderedType *)
-let cOrderedTypeCompare =
-  gen_constant [["Coq";"Structures";"OrderedType"]] "Compare"
+(* let cOrderedTypeCompare =
+ *   gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *)
 
 (* SMT_terms *)
 let smt_modules = [ ["SMTCoq";"Misc"];
@@ -172,7 +173,7 @@ let cTBV = gen_constant smt_modules "TBV"
 let cTFArray = gen_constant smt_modules "TFArray"
 let cTindex = gen_constant smt_modules "Tindex"
 
-let ct_i = gen_constant smt_modules "t_i"
+(* let ct_i = gen_constant smt_modules "t_i" *)
 let cinterp_t = gen_constant smt_modules "Typ.interp"
 let cdec_interp = gen_constant smt_modules "dec_interp"
 let cord_interp = gen_constant smt_modules "ord_interp"
@@ -180,14 +181,14 @@ let ccomp_interp = gen_constant smt_modules "comp_interp"
 let cinh_interp = gen_constant smt_modules "inh_interp"
 
 let cinterp_eqb = gen_constant smt_modules "i_eqb"
-let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb"
+(* let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" *)
 
 let classes_modules = [["SMTCoq";"classes";"SMT_classes"];
                        ["SMTCoq";"classes";"SMT_classes_instances"]]
 
 let ctyp_compdec = gen_constant classes_modules "typ_compdec"
 let cTyp_compdec = gen_constant classes_modules "Typ_compdec"
-let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from"
+(* let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" *)
 let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec"
 let cte_carrier = gen_constant classes_modules "te_carrier"
 let cte_compdec = gen_constant classes_modules "te_compdec"
@@ -340,7 +341,7 @@ let mkN = function
   | i -> SmtMisc.mklApp cNpos [|mkPositive i|]
 
 (* Compute a Boolean *)
-let rec mkBool = function
+let mkBool = function
   | true -> Lazy.force ctrue
   | false -> Lazy.force cfalse
 
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index b21bef8..9aeddac 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -259,4 +259,5 @@ val mk_bool : Term.constr -> bool
 val mk_bool_list : Term.constr -> bool list
 val mk_nat : Term.constr -> int
 val mk_N : Term.constr -> int
+val mk_Z : Term.constr -> int
 val mk_bvsize : Term.constr -> int
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index b5fe759..4ecfae3 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -21,7 +21,6 @@ module Atom : sig
   val to_smt : Format.formatter -> t -> unit
   val logic : t -> SmtMisc.logic
 
-  val is_bool_type : t -> bool
   type reify_tbl = {
       mutable count : int;
       tbl : (Term.constr, t) Hashtbl.t;
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index fd9f2bd..330884b 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -12,9 +12,6 @@
 
 open SmtMisc
 open CoqTerms
-open Entries
-open Declare
-open Decl_kinds
 open SmtBtype
 
 
@@ -229,8 +226,8 @@ module Op =
       | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te))
 
 
-    let interp_ieq t_i t =
-      mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|]
+    (* let interp_ieq t_i t =
+     *   mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] *)
 
  (*   let veval_t te =
       let env = Global.env () in
@@ -246,30 +243,30 @@ module Op =
 
     let interp_eqarray t_i ti te =
       mklApp cequalarray
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
-                SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+          SmtBtype.inh_interp t_i te |]
 
     let interp_select t_i ti te =
       mklApp cselect
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.inh_interp t_i te|]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.inh_interp t_i te|]
 
     let interp_diff t_i ti te =
       mklApp cdiff
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
-                SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+          SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]
 
 
     let interp_store t_i ti te =
       mklApp cstore
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]
 
 
     let interp_eq t_i = function
@@ -1022,7 +1019,7 @@ module Atom =
           else CCunknown_deps (gobble_of_coq_cst cc)
         with Not_found -> CCunknown
       in
-      let rec mk_hatom h =
+      let rec mk_hatom (h : Term.constr) =
         let c, args = Term.decompose_app h in
 	match get_cst c with
         | CCxH -> mk_cop CCxH args
@@ -1064,9 +1061,9 @@ module Atom =
         | CCselect -> mk_bop_select args
         | CCdiff -> mk_bop_diff args
         | CCstore -> mk_top_store args
-	| CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
+	| CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h)
         | CCunknown_deps gobble ->
-          mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble
+          mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble
 
 
       and mk_cop op args = match op, args with
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 0ebb893..119c046 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -119,8 +119,8 @@ let to_list reify =
 let make_t_i rt = interp_tbl rt
 
 
-let interp_t t_i t =
-  mklApp cinterp_t [|t_i ; to_coq t|]
+(* let interp_t t_i t =
+ *   mklApp cinterp_t [|t_i ; to_coq t|] *)
 
 let dec_interp t_i t =
   mklApp cdec_interp [|t_i ; to_coq t|]
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index b1468e4..6ce6997 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -10,8 +10,6 @@
 (**************************************************************************)
 
 
-open SmtForm
-
 type used = int
 
 type clause_id  = int
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 43365ef..1a990f1 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -34,10 +34,10 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
 let cchecker_eq_correct =
   gen_constant euf_checker_modules "checker_eq_correct"
 let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-let csetup_checker_step_debug =
-  gen_constant euf_checker_modules "setup_checker_step_debug"
-let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug"
-let cstep = gen_constant euf_checker_modules "step"
+(* let csetup_checker_step_debug =
+ *   gen_constant euf_checker_modules "setup_checker_step_debug" *)
+(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *)
+(* let cstep = gen_constant euf_checker_modules "step" *)
 let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
 
 let cname_step = gen_constant euf_checker_modules "name_step"
@@ -315,7 +315,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
    Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
    mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
 
-  let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+  let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
   Format.eprintf "     = %s\n     : bool@."
     (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
         "true" else "false")
@@ -389,7 +389,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
    mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*);
        v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
 
-  let res = Vnorm.cbv_vm (Global.env ()) tm
+  let res = Structures.cbv_vm (Global.env ()) tm
       (mklApp coption
          [|mklApp cprod
              [|Lazy.force cnat; Lazy.force cname_step|]|]) in
@@ -453,117 +453,117 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
 
 
 
-let rec of_coq_list cl =
-  match Term.decompose_app cl with
-  | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
-  | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
-    x :: of_coq_list cr
-  | _ -> assert false
-
-
-let checker_debug_step t_i t_func t_atom t_form root used_root trace
-    (rt, ro, ra, rf, roots, max_id, confl) =
-
-  let t_i' = make_t_i rt in
-  let ce5 = Structures.mkUConst t_i' in
-  let ct_i = Term.mkConst (declare_constant t_i
-                             (DefinitionEntry ce5, IsDefinition Definition)) in
-
-  let t_func' = make_t_func ro ct_i in
-  let ce6 = Structures.mkUConst t_func' in
-  let ct_func =
-    Term.mkConst (declare_constant t_func
-                    (DefinitionEntry ce6, IsDefinition Definition)) in
-
-  let t_atom' = Atom.interp_tbl ra in
-  let ce1 = Structures.mkUConst t_atom' in
-  let ct_atom =
-    Term.mkConst (declare_constant t_atom
-                    (DefinitionEntry ce1, IsDefinition Definition)) in
-
-  let t_form' = snd (Form.interp_tbl rf) in
-  let ce2 = Structures.mkUConst t_form' in
-  let ct_form =
-    Term.mkConst (declare_constant t_form
-                    (DefinitionEntry ce2, IsDefinition Definition)) in
-
-  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
-      (interp_conseq_uf ct_i)
-      (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
-  List.iter (fun (v,ty) ->
-    let _ = Structures.declare_new_variable v ty in
-    print_assm ty
-  ) cuts;
-
-  let used_roots = compute_roots roots last_root in
-  let croots =
-    let res = Array.make (List.length roots + 1) (mkInt 0) in
-    let i = ref 0 in
-    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    Structures.mkArray (Lazy.force cint, res) in
-  let cused_roots =
-    let l = List.length used_roots in
-    let res = Array.make (l + 1) (mkInt 0) in
-    let i = ref (l-1) in
-    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
-    mklApp cSome [|mklApp carray [|Lazy.force cint|];
-                   Structures.mkArray (Lazy.force cint, res)|] in
-  let ce3 = Structures.mkUConst croots in
-  let _ = declare_constant root
-      (DefinitionEntry ce3, IsDefinition Definition) in
-  let ce3' = Structures.mkUConst cused_roots in
-  let _ = declare_constant used_root
-      (DefinitionEntry ce3', IsDefinition Definition) in
-
-  let certif =
-    mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
-                     tres;mkInt (get_pos confl)|] in
-  let ce4 = Structures.mkUConst certif in
-  let _ = declare_constant trace
-      (DefinitionEntry ce4, IsDefinition Definition) in
-
-  let setup =
-   mklApp csetup_checker_step_debug
-     [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
-
-  let setup = Vnorm.cbv_vm (Global.env ()) setup
-      (mklApp cprod
-         [|Lazy.force cState_S_t;
-           mklApp clist [|mklApp cstep
-                            [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
-
-  let s, steps = match Term.decompose_app setup with
-    | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
-      s, of_coq_list csteps
-    | _ -> assert false
-  in
-
-  let cpt = ref (List.length roots) in
-  let debug_step s step =
-    incr cpt;
-    Format.eprintf "%d@." !cpt;
-    let tm =
-      mklApp cchecker_step_debug
-        [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
-
-    let res =
-      Vnorm.cbv_vm (Global.env ()) tm
-          (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
-
-    match Term.decompose_app res with
-    | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
-      if not (mk_bool cbad) then s
-      else Structures.error ("Step number " ^ string_of_int !cpt ^
-                             " (" ^ string_coq_constr
-                               (fst (Term.decompose_app step)) ^ ")" ^
-                             " of the certificate likely failed." )
-    | _ -> assert false
-  in
-
-  List.fold_left debug_step s steps |> ignore;
-
-  Structures.error ("Debug checker is only meant to be used for certificates \
-                     that fail to be checked by SMTCoq.")
+(* let rec of_coq_list cl =
+ *   match Term.decompose_app cl with
+ *   | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
+ *   | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+ *     x :: of_coq_list cr
+ *   | _ -> assert false *)
+
+
+(* let checker_debug_step t_i t_func t_atom t_form root used_root trace
+ *     (rt, ro, ra, rf, roots, max_id, confl) =
+ * 
+ *   let t_i' = make_t_i rt in
+ *   let ce5 = Structures.mkUConst t_i' in
+ *   let ct_i = Term.mkConst (declare_constant t_i
+ *                              (DefinitionEntry ce5, IsDefinition Definition)) in
+ * 
+ *   let t_func' = make_t_func ro ct_i in
+ *   let ce6 = Structures.mkUConst t_func' in
+ *   let ct_func =
+ *     Term.mkConst (declare_constant t_func
+ *                     (DefinitionEntry ce6, IsDefinition Definition)) in
+ * 
+ *   let t_atom' = Atom.interp_tbl ra in
+ *   let ce1 = Structures.mkUConst t_atom' in
+ *   let ct_atom =
+ *     Term.mkConst (declare_constant t_atom
+ *                     (DefinitionEntry ce1, IsDefinition Definition)) in
+ * 
+ *   let t_form' = snd (Form.interp_tbl rf) in
+ *   let ce2 = Structures.mkUConst t_form' in
+ *   let ct_form =
+ *     Term.mkConst (declare_constant t_form
+ *                     (DefinitionEntry ce2, IsDefinition Definition)) in
+ * 
+ *   let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ *       (interp_conseq_uf ct_i)
+ *       (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+ *   List.iter (fun (v,ty) ->
+ *     let _ = Structures.declare_new_variable v ty in
+ *     print_assm ty
+ *   ) cuts;
+ * 
+ *   let used_roots = compute_roots roots last_root in
+ *   let croots =
+ *     let res = Array.make (List.length roots + 1) (mkInt 0) in
+ *     let i = ref 0 in
+ *     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+ *     Structures.mkArray (Lazy.force cint, res) in
+ *   let cused_roots =
+ *     let l = List.length used_roots in
+ *     let res = Array.make (l + 1) (mkInt 0) in
+ *     let i = ref (l-1) in
+ *     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+ *     mklApp cSome [|mklApp carray [|Lazy.force cint|];
+ *                    Structures.mkArray (Lazy.force cint, res)|] in
+ *   let ce3 = Structures.mkUConst croots in
+ *   let _ = declare_constant root
+ *       (DefinitionEntry ce3, IsDefinition Definition) in
+ *   let ce3' = Structures.mkUConst cused_roots in
+ *   let _ = declare_constant used_root
+ *       (DefinitionEntry ce3', IsDefinition Definition) in
+ * 
+ *   let certif =
+ *     mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
+ *                      tres;mkInt (get_pos confl)|] in
+ *   let ce4 = Structures.mkUConst certif in
+ *   let _ = declare_constant trace
+ *       (DefinitionEntry ce4, IsDefinition Definition) in
+ * 
+ *   let setup =
+ *    mklApp csetup_checker_step_debug
+ *      [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
+ * 
+ *   let setup = Structures.cbv_vm (Global.env ()) setup
+ *       (mklApp cprod
+ *          [|Lazy.force cState_S_t;
+ *            mklApp clist [|mklApp cstep
+ *                             [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
+ * 
+ *   let s, steps = match Term.decompose_app setup with
+ *     | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+ *       s, of_coq_list csteps
+ *     | _ -> assert false
+ *   in
+ * 
+ *   let cpt = ref (List.length roots) in
+ *   let debug_step s step =
+ *     incr cpt;
+ *     Format.eprintf "%d@." !cpt;
+ *     let tm =
+ *       mklApp cchecker_step_debug
+ *         [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
+ * 
+ *     let res =
+ *       Structures.cbv_vm (Global.env ()) tm
+ *           (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
+ * 
+ *     match Term.decompose_app res with
+ *     | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+ *       if not (mk_bool cbad) then s
+ *       else Structures.error ("Step number " ^ string_of_int !cpt ^
+ *                              " (" ^ string_coq_constr
+ *                                (fst (Term.decompose_app step)) ^ ")" ^
+ *                              " of the certificate likely failed." )
+ *     | _ -> assert false
+ *   in
+ * 
+ *   List.fold_left debug_step s steps |> ignore;
+ * 
+ *   Structures.error ("Debug checker is only meant to be used for certificates \
+ *                      that fail to be checked by SMTCoq.") *)
 
 
 
@@ -725,7 +725,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
 
   let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
   let lcpl = lcpl @ tlcepl in
-  let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
+  let lcl = List.map (Structures.retyping_get_type_of env sigma) lcpl in
 
   let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
   let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 4138e7c..ad6a5a4 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -618,7 +618,7 @@ module Make (Atom:ATOM) =
 		             mklApp cifb (Array.map interp_form args)
 		          | Fnot2 n ->
 		             (let r = ref (interp_form args.(0)) in
-		              for i = 1 to n do
+		              for _ = 1 to n do
                                 r := mklApp cnegb [|!r|]
                               done;
                               !r)
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b410f88..a9855a2 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -409,12 +409,12 @@ let to_coq to_lit interp (cstep,
           mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|]
 	| LiaMicromega (cl,d) ->
           let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
-          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in
           mklApp cLiaMicromega [|out_c c; cl'; c'|]
         | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|]
         | SplArith (orig,res,l) ->
           let res' = out_f res in
-          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in
           mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
 	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
         | BBVar res -> mklApp cBBVar [|out_c c; out_f res|]
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 32f76f1..2fd7d2d 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -10,55 +10,50 @@
 (**************************************************************************)
 
 
-open Entries
-open Declare
-open Decl_kinds
-
 open SmtMisc
 open CoqTerms
-open SmtForm
 open SmtTrace
 open SmtAtom
 open SmtBtype
 open SmtCertif
 
 
-let debug = false
+(* let debug = false *)
 
 
 (******************************************************************************)
 (* Given a verit trace build the corresponding certif and theorem             *)
 (******************************************************************************)
-exception Import_trace of int
+(* exception Import_trace of int *)
 
-let get_val = function
-    Some a -> a
-  | None -> assert false
+(* let get_val = function
+ *     Some a -> a
+ *   | None -> assert false *)
 
 (* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
-let print_certif c where=
-  let r = ref c in
-  let out_channel = open_out where in
-  let fmt = Format.formatter_of_out_channel out_channel in
-  let continue = ref true in
-  while !continue do
-    let kind = to_string (!r.kind) in
-    let id = !r.id in
-    let pos = match !r.pos with
-      | None -> "None"
-      | Some p -> string_of_int p in
-    let used = !r.used in
-    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
-    begin match !r.value with
-    | None -> Format.fprintf fmt "None"
-    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_smt fmt f;
-                                    Format.fprintf fmt " ") l end;
-    Format.fprintf fmt "\n";
-    match !r.next with
-    | None -> continue := false
-    | Some n -> r := n
-  done;
-  Format.fprintf fmt "@."; close_out out_channel
+(* let print_certif c where=
+ *   let r = ref c in
+ *   let out_channel = open_out where in
+ *   let fmt = Format.formatter_of_out_channel out_channel in
+ *   let continue = ref true in
+ *   while !continue do
+ *     let kind = to_string (!r.kind) in
+ *     let id = !r.id in
+ *     let pos = match !r.pos with
+ *       | None -> "None"
+ *       | Some p -> string_of_int p in
+ *     let used = !r.used in
+ *     Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
+ *     begin match !r.value with
+ *     | None -> Format.fprintf fmt "None"
+ *     | Some l -> List.iter (fun f -> Form.to_smt Atom.to_smt fmt f;
+ *                                     Format.fprintf fmt " ") l end;
+ *     Format.fprintf fmt "\n";
+ *     match !r.next with
+ *     | None -> continue := false
+ *     | Some n -> r := n
+ *   done;
+ *   Format.fprintf fmt "@."; close_out out_channel *)
 
 let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index e209fd2..6b26f65 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -193,18 +193,18 @@ let mkDistinctElim old value =
 
 (* Clause difference (wrt to their sets of literals) *)
 
-let clause_diff c1 c2 =
-  let r =
-    List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
-  in
-  Format.eprintf "[";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
-  Format.eprintf "] -- [";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
-  Format.eprintf "] ==\n [";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
-  Format.eprintf "] @.";
-  r
+(* let clause_diff c1 c2 =
+ *   let r =
+ *     List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
+ *   in
+ *   Format.eprintf "[";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
+ *   Format.eprintf "] -- [";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
+ *   Format.eprintf "] ==\n [";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
+ *   Format.eprintf "] @.";
+ *   r *)
 
 
 
@@ -234,7 +234,7 @@ let rec fins_lemma ids_params =
                 Other (Forall_inst (lemma, _)) -> lemma
               | _ -> fins_lemma t
 
-let rec find_remove_lemma lemma ids_params =
+let find_remove_lemma lemma ids_params =
   let eq_lemma h = eq_clause lemma (get_clause h) in
   list_find_remove eq_lemma ids_params
 
@@ -250,7 +250,7 @@ let rec merge ids_params =
 
 let to_add = ref []
 
-let rec mk_clause (id,typ,value,ids_params) =
+let mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
       (* Roots *)
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
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 2bbb23d..11989c5 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -14,7 +14,6 @@ open Entries
 open Declare
 open Decl_kinds
 
-open SmtMisc
 open CoqTerms
 open SmtForm
 open SmtCertif
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index 4c312fc..6314927 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -10,6 +10,7 @@
 (**************************************************************************)
 
 
+val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
 val parse_certif : Structures.names_id -> Structures.names_id -> string -> string -> unit
 val checker : string -> string -> unit
 val theorem : Structures.names_id -> string -> string -> unit
diff --git a/src/zchaff/zchaffParser.ml b/src/zchaff/zchaffParser.ml
index c4a2f62..e3db7b6 100644
--- a/src/zchaff/zchaffParser.ml
+++ b/src/zchaff/zchaffParser.ml
@@ -11,7 +11,6 @@
 
 
 open SatParser
-open SmtForm
 open SmtCertif
 open SmtTrace
 
@@ -58,7 +57,7 @@ let parse_CL reloc lb last =
 
 (* Parsing of the VAR and CONF part *)
 
-let var_of_lit l = l lsr 1
+(* let var_of_lit l = l lsr 1 *)
 
 type var_key =
   | Var of int
diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v
index 05a9fb4..c868864 100644
--- a/unit-tests/Tests_lfsc.v
+++ b/unit-tests/Tests_lfsc.v
@@ -15,6 +15,8 @@ Add Rec LoadPath "../src" as SMTCoq.
 Require Import SMTCoq.
 Require Import Bool PArray Int63 List ZArith Logic.
 
+Local Open Scope Z_scope.
+
 
 Infix "-->" := implb (at level 60, right associativity) : bool_scope.
 
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index f374b1b..002854c 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -16,49 +16,9 @@ Require Import SMTCoq.
 Require Import Bool PArray Int63 List ZArith.
 
 Local Open Scope int63_scope.
-
-(* First a tactic, to test the universe computation in an empty
-   environment. *)
-
-Lemma check_univ (x1: bool):
-  (x1 && (negb x1)) = false.
-Proof.
-  verit.
-Qed.
-
-(* (* In standard coq we need decidability of Int31.digits *) *)
-(* Lemma fun_const : *)
-(*   forall f (g : int -> int -> bool), *)
-(*     (forall x, g (f x) 2) -> g (f 3) 2. *)
-(* Proof. *)
-(*   intros f g Hf. *)
-(*   verit Hf. *)
-(*   -admit. *)
-(*   (* a proof that there is a decidable equality on digits : *) *)
-(*   (* exists (fun x y => match (x, y) with (Int31.D0, Int31.D0)
-| (Int31.D1, Int31.D1) => true | _ => false end). *) *)
-(*   (* intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *) *)
-(*   (* exists Int63Native.eqb. *) *)
-(*   (* apply Int63Properties.reflect_eqb. *) *)
-(*   -apply int63_compdec. *)
-
-
 Open Scope Z_scope.
 
 
-Lemma fun_const2 :
-  forall f (g : Z -> Z -> bool),
-    (forall x, g (f x) 2) -> g (f 3) 2.
-Proof.
-  intros f g Hf. verit Hf.
-Qed.
-(*
-Toplevel input, characters 916-942:
- Warning: Bytecode compiler failed, falling back to standard conversion
- [bytecode-compiler-failed,bytecode-compiler]
-*)
-
-
 (* veriT vernacular commands *)
 
 Section Checker_Sat0.
@@ -540,6 +500,20 @@ End Theorem_Bv2.
 
 (* verit tactic *)
 
+Lemma check_univ (x1: bool):
+  (x1 && (negb x1)) = false.
+Proof.
+  verit.
+Qed.
+
+Lemma fun_const2 :
+  forall f (g : Z -> Z -> bool),
+    (forall x, g (f x) 2) -> g (f 3) 2.
+Proof.
+  intros f g Hf. verit Hf.
+Qed.
+
+
 (* Simple connectives *)
 
 Goal forall (a:bool), a || negb a.