From a88e3b3b6ad01a9b85c828b9a1225732275affee Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Mon, 11 Mar 2019 20:25:35 +0100
Subject: V8.8 (#42)

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Organization structures

* 8.8 ok with standard coq
---
 src/Conversion_tactics.v                           |  12 +-
 src/Misc.v                                         | 118 +++---
 src/SMT_terms.v                                    |   4 +-
 src/array/Array_checker.v                          |   6 +-
 src/array/FArray.v                                 |   5 +-
 src/classes/SMT_classes_instances.v                |  13 +-
 src/lia/Lia.v                                      |  22 +-
 src/smtlib2/smtlib2_genConstr.ml                   |   6 +-
 src/trace/coqTerms.ml                              |  73 ++--
 src/trace/coqTerms.mli                             | 424 ++++++++++-----------
 src/trace/satAtom.ml                               |   2 +-
 src/trace/satAtom.mli                              |  10 +-
 src/trace/smtAtom.ml                               |  32 +-
 src/trace/smtAtom.mli                              |  26 +-
 src/trace/smtBtype.ml                              |  38 +-
 src/trace/smtBtype.mli                             |  32 +-
 src/trace/smtCommands.ml                           | 340 ++++++++---------
 src/trace/smtCommands.mli                          |  20 +-
 src/trace/smtForm.ml                               |  30 +-
 src/trace/smtForm.mli                              |  46 ++-
 src/trace/smtMisc.ml                               |  16 +-
 src/trace/smtMisc.mli                              |  13 +-
 src/trace/smtTrace.ml                              |   8 +-
 src/trace/smtTrace.mli                             |  38 +-
 src/verit/verit.mli                                |  16 +-
 src/versions/native/structures.ml                  | 155 ++++----
 src/versions/native/structures.mli                 | 131 ++++---
 src/versions/standard/Int63/Int63Axioms_standard.v |   2 +-
 .../standard/Int63/Int63Properties_standard.v      | 107 +++---
 src/versions/standard/Make                         |   2 +-
 src/versions/standard/structures.ml                | 218 ++++++-----
 src/versions/standard/structures.mli               | 143 ++++---
 src/zchaff/zchaff.ml                               |  95 +++--
 src/zchaff/zchaff.mli                              |   6 +-
 34 files changed, 1146 insertions(+), 1063 deletions(-)

diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
index 37a39b5..4a791e6 100644
--- a/src/Conversion_tactics.v
+++ b/src/Conversion_tactics.v
@@ -102,7 +102,7 @@ Ltac converting :=
   repeat
     match goal with
     (* On capture chaque sous-terme x avec son contexte, i.e. le but est C[x] *)
-    | |- appcontext C[?x]  =>
+    | |- context C[?x]  =>
       (* Si x est de type T *)
       let U := type of x in
       lazymatch eval fold T in U with
@@ -116,7 +116,7 @@ Ltac converting :=
           pose proof x as var;
           (* Sinon, on analyse la formule obtenue en remplaçant x par notre variable fraîche dans le but *)
           lazymatch context C[var] with
-          | appcontext [?h var] =>
+          | context [?h var] =>
             let h := get_head h in
             lazymatch h with
             (* x est déjà réécrit *)
@@ -201,7 +201,7 @@ Ltac renaming :=
   repeat
     match goal with
       (* S'il y a un terme de la forme (T2Z (f t1 ... tn)) *)
-      | |- appcontext [T2Z ?X] =>
+      | |- context [T2Z ?X] =>
         (* On récupère le symbole de tête *)
         let f := get_head X in
         (* S'il s'agit d'un constructeur on ne fait rien *)
@@ -214,7 +214,7 @@ Ltac renaming :=
         repeat
           match goal with
             (* Pour chaque terme de la forme (T2Z (f' t'1 ... t'n)) *)
-            | |- appcontext [T2Z ?X'] =>
+            | |- context [T2Z ?X'] =>
               (* On récupère le symbole de tête *)
               let f' := get_head X' in
               (* Si f' = f *)
@@ -269,7 +269,7 @@ Ltac renaming' :=
   repeat
     match goal with
       (* S'il y a un terme de la forme (f t1 ... (Z2T tn)) *)
-      | |- appcontext [?X (Z2T ?Y)] =>
+      | |- context [?X (Z2T ?Y)] =>
         (* On récupère le symbole de tête *)
         let f := get_head X in
         (* S'il s'agit d'un constructeur on ne fait rien *)
@@ -280,7 +280,7 @@ Ltac renaming' :=
         repeat
           match goal with
             (* Pour chaque terme de la forme (f' t'1 ... (Z2T t'n)) *)
-            | |- appcontext [?X' (Z2T ?Y')] =>
+            | |- context [?X' (Z2T ?Y')] =>
               (* On récupère le symbole de tête *)
               let f' := get_head X' in
               (* Si f' = f *)
diff --git a/src/Misc.v b/src/Misc.v
index 84feab4..5fc6602 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import Bool List PArray Int63 ZArith.
+Require Import Bool List PArray Int63 ZArith Psatz.
 Local Open Scope int63_scope.
 Local Open Scope array_scope.
 
@@ -30,12 +30,12 @@ Proof.
   rewrite <- leb_spec in H; rewrite H; discriminate.
   intros H1 _; apply to_Z_inj; rewrite add_spec, to_Z_1 in H.
   assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB).
-  pose (H3 := to_Z_bounded j); omega.
+  pose (H3 := to_Z_bounded j); lia.
   destruct H2 as [H2|H2].
   rewrite Zmod_small in H.
-  omega.
+  lia.
   split.
-  pose (H3 := to_Z_bounded j); omega.
+  pose (H3 := to_Z_bounded j); lia.
   assumption.
   rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption.
 Qed.
@@ -48,14 +48,14 @@ Proof.
   rewrite <- ltb_spec in H; rewrite H; discriminate.
   intros H1 _; apply to_Z_inj. rewrite add_spec in H1. rewrite to_Z_1 in H1.
   assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB).
-  pose (H3 := to_Z_bounded j); omega.
+  pose (H3 := to_Z_bounded j); lia.
   destruct H2 as [H2|H2].
   rewrite Zmod_small in H1.
-  omega.
+  lia.
   split.
-  pose (H3 := to_Z_bounded j); omega.
+  pose (H3 := to_Z_bounded j); lia.
   assumption.
-  rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. omega.
+  rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia.
 Qed.
 
 
@@ -74,19 +74,19 @@ Proof.
                        min (fun a0 : A => a0))).
  apply foldi_down_cont_ZInd;intros;red.
  assert (H20: (z+1 < [|min|]+1)%Z).
- omega.
+ lia.
  rewrite Zlt_is_lt_bool in H20; rewrite H20;trivial.
  case_eq (Zlt_bool ([|i|]+1) ([|min|]+1));intros.
-  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;lia.
  clear H4;revert H3;unfold P'.
  case_eq (Zlt_bool ([|i|] - 1 + 1) ([|min|]+1));intros;auto.
-  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;omega).
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;lia).
   rewrite H4, <- H6. apply H0;trivial.
-  apply H4. replace ([|i|] - 1 + 1)%Z with [|i|] by omega. auto.
+  apply H4. replace ([|i|] - 1 + 1)%Z with [|i|] by lia. auto.
  revert H1;unfold P'.
  case_eq (Zlt_bool ([|max|]+1)%Z ([|min|]+1)%Z);auto.
  rewrite <- Zlt_is_lt_bool.
- intro H22; assert (H21: ([|max|] < [|min|])%Z). omega.
+ intro H22; assert (H21: ([|max|] < [|min|])%Z). lia.
  rewrite <- ltb_spec in H21. intros;rewrite foldi_down_cont_lt;auto.
 Qed.
 
@@ -120,26 +120,26 @@ Lemma to_list_In : forall {A} (t: array A) i,
   i < length t = true -> In (t.[i]) (to_list t).
 Proof.
   intros A t i H; unfold to_list; case_eq (0 == length t); intro Heq.
-  unfold is_true in H; rewrite ltb_spec in H; rewrite eqb_spec in Heq; rewrite <- Heq in H; rewrite to_Z_0 in H; pose (H1 := to_Z_bounded i); elimtype False; omega.
+  unfold is_true in H; rewrite ltb_spec in H; rewrite eqb_spec in Heq; rewrite <- Heq in H; rewrite to_Z_0 in H; pose (H1 := to_Z_bounded i); elimtype False; lia.
   pose (P := fun j a => i < j = true \/ In (t .[ i]) a).
   pose (H1:= foldi_down_Ind2 _ P); unfold P in H1.
   assert (H2: i < 0 = true \/ In (t .[ i]) (foldi_down (fun (i0 : int) (l : list A) => t .[ i0] :: l) (length t - 1) 0 nil)).
   apply H1.
   rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption.
-  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; omega.
-  intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); omega.
+  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia.
+  intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); lia.
   left; unfold is_true; rewrite ltb_spec; rewrite (to_Z_add_1 _ max_int).
   erewrite to_Z_sub_1; try eassumption.
-  unfold is_true in H; rewrite ltb_spec in H; omega.
+  unfold is_true in H; rewrite ltb_spec in H; lia.
   rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption.
-  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; omega.
+  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia.
   intros j a H2 H3 [H4|H4].
   case_eq (i < j); intro Heq2.
   left; reflexivity.
   right; rewrite (lt_eq _ _ H4 Heq2); constructor; reflexivity.
   right; constructor 2; assumption.
   destruct H2 as [H2|H2]; try assumption.
-  unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; omega.
+  unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia.
 Qed.
 
 Lemma In_to_list : forall {A} (t: array A) x,
@@ -151,11 +151,11 @@ Proof.
   pose (P (_:int) l := In x l ->
    exists i : int, (i < length t) = true /\ x = t .[ i]).
   pose (H1 := foldi_down_Ind2 _ P (fun (i : int) (l : list A) => t .[ i] :: l) (length t - 1) 0); unfold P in H1; apply H1.
-  rewrite ltb_spec, to_Z_sub_1_diff; auto; change [|max_int|] with (wB-1)%Z; pose (H2 := to_Z_bounded (length t)); omega.
+  rewrite ltb_spec, to_Z_sub_1_diff; auto; change [|max_int|] with (wB-1)%Z; pose (H2 := to_Z_bounded (length t)); lia.
   intros _ H; inversion H.
   intro H; inversion H.
   simpl; intros i a _ H2 IH [H3|H3].
-  exists i; split; auto; rewrite ltb_spec; rewrite leb_spec, to_Z_sub_1_diff in H2; auto; omega.
+  exists i; split; auto; rewrite ltb_spec; rewrite leb_spec, to_Z_sub_1_diff in H2; auto; lia.
   destruct (IH H3) as [j [H4 H5]]; exists j; auto.
 Qed.
 
@@ -190,17 +190,17 @@ Proof.
   rewrite Int63Properties.eqb_spec; intro Heq; rewrite Heq in Hi; eelim ltb_0; eassumption.
   rewrite eqb_false_spec; intro Heq; pose (Hi':=Hi); replace (length t) with ((length t - 1) + 1) in Hi'.
   generalize Hi'; apply (foldi_Ind _ (fun j a => (i < j) = true -> length a = length t -> a.[i] = f i (t.[i]))).
-  rewrite ltb_spec, (to_Z_sub_1 _ i); auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; omega.
+  rewrite ltb_spec, (to_Z_sub_1 _ i); auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia.
   intros H _; eelim ltb_0; eassumption.
   intros H; eelim ltb_0; eassumption.
   intros j a _ H1 IH H2 H3; rewrite length_set in H3; case_eq (j == i).
   rewrite Int63Properties.eqb_spec; intro Heq2; subst i; rewrite get_set_same; auto; rewrite H3; auto.
   rewrite eqb_false_spec; intro Heq2; rewrite get_set_other; auto; apply IH; auto; rewrite ltb_spec; rewrite ltb_spec, (to_Z_add_1 _ (length t)) in H2.
-  assert (H4: [|i|] <> [|j|]) by (intro H4; apply Heq2, to_Z_inj; auto); omega.
-  rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; omega.
+  assert (H4: [|i|] <> [|j|]) by (intro H4; apply Heq2, to_Z_inj; auto); lia.
+  rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; lia.
   apply to_Z_inj; rewrite (to_Z_add_1 _ max_int).
-  rewrite to_Z_sub_1_diff; auto; omega.
-  rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; omega.
+  rewrite to_Z_sub_1_diff; auto; lia.
+  rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia.
 Qed.
 
 
@@ -268,7 +268,7 @@ Proof.
   rewrite ltb_spec, to_Z_sub_1_diff; auto with zarith.
   intro H3; rewrite H3 in Heq; discriminate.
   intro Hlt; assert (H3: length t - 1 = 0).
-  rewrite ltb_spec, to_Z_1 in Hlt; apply to_Z_inj; rewrite to_Z_0; pose (H3 := to_Z_bounded (length t - 1)); omega.
+  rewrite ltb_spec, to_Z_1 in Hlt; apply to_Z_inj; rewrite to_Z_0; pose (H3 := to_Z_bounded (length t - 1)); lia.
   rewrite H3; assumption.
   intros i a H3 H4; apply H1; trivial.
   rewrite ltb_leb_sub1; auto.
@@ -321,7 +321,7 @@ Lemma afold_left_spec : forall A B (f:B -> A) args op e,
     assert (H1: length args = 1).
     generalize (to_Z_bounded (length args)).
     rewrite <- not_true_iff_false, ltb_spec, to_Z_0, to_Z_sub_1_diff in H;auto.
-    intros;apply to_Z_inj;rewrite to_Z_1;omega.
+    intros;apply to_Z_inj;rewrite to_Z_1;lia.
     rewrite H1; change (1 - 1) with 0; rewrite (foldi_eq _ _ 0 0); auto.
   Qed.
 
@@ -347,7 +347,7 @@ Proof.
   apply ltb_leb_sub1;trivial.
   revert n0 H3;rewrite ltb_spec, leb_spec, to_Z_1, sub_spec.
   change [|2|] with 2%Z.
-  intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;omega.
+  intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;lia.
 Qed.
 
 
@@ -379,10 +379,10 @@ Proof.
   rewrite to_Z_sub_1_diff.
   ring_simplify ([|length t - 1|] - 1 + 1)%Z;rewrite of_to_Z;trivial.
   assert (H10: (1 < length t) = true) by (rewrite ltb_negb_geb, Heq; auto).
-  intro H11. rewrite ltb_spec in H10. assert (H12: [|length t - 1|] = 0%Z) by (rewrite H11; auto). change [|1|] with (1%Z) in H10. rewrite to_Z_sub_1_diff in H12; [omega| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). omega.
+  intro H11. rewrite ltb_spec in H10. assert (H12: [|length t - 1|] = 0%Z) by (rewrite H11; auto). change [|1|] with (1%Z) in H10. rewrite to_Z_sub_1_diff in H12; [lia| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). lia.
   intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto.
   assert (i < length t - 1 = true).
-    rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [omega| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [omega| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). omega.
+    rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [lia| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [lia| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). lia.
   apply H1; [trivial| ].
   rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto.
   symmetry. rewrite eqb_false_spec. intro H. rewrite H in Heq. discriminate.
@@ -412,7 +412,7 @@ Proof.
   intros A B P default OP F t H1 H2 H4.
   pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t).
   unfold afold_right. case_eq (length t == 0); auto. intro H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq.
-  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
+  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
 Qed.
 
 
@@ -425,7 +425,7 @@ Proof.
   intros A B P default OP F t H1 H2 H4.
   pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t).
   unfold afold_right. assert (H10 : length t == 0 = false) by (rewrite eqb_false_spec; intro H; rewrite H in H2; discriminate). rewrite H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq.
-  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
+  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
 Qed.
 
 
@@ -440,11 +440,11 @@ Lemma afold_right_spec : forall A B (f:B -> A) args op e,
     apply not_eq_sym in n;rewrite (eqb_false_complete _ _ n).
     case_eq (length args <= 1); intro Heq.
     assert (H11: length args = 1).
-    apply to_Z_inj. rewrite leb_spec in Heq. assert (H11: 0%Z <> [|length args|]) by (intro H; elim n; apply to_Z_inj; auto). change [|1|] with (1%Z) in *. assert (H12 := leb_0 (length args)). rewrite leb_spec in H12. change [|0|] with 0%Z in H12. omega.
+    apply to_Z_inj. rewrite leb_spec in Heq. assert (H11: 0%Z <> [|length args|]) by (intro H; elim n; apply to_Z_inj; auto). change [|1|] with (1%Z) in *. assert (H12 := leb_0 (length args)). rewrite leb_spec in H12. change [|0|] with 0%Z in H12. lia.
     rewrite H11, foldi_down_eq; auto.
     assert (H11: 1 < length args = true) by (rewrite ltb_negb_geb, Heq; auto). replace (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1) 0 neu) with (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1 - 1) 0 (op (f (args .[ length args - 1])) neu)).
     replace (length args - 1 - 1) with (length args - 2) by ring. rewrite H10. auto.
-    symmetry. apply foldi_down_gt. rewrite ltb_spec. change [|0|] with 0%Z. rewrite to_Z_sub_1_diff; auto. rewrite ltb_spec in H11. change [|1|] with 1%Z in H11. omega.
+    symmetry. apply foldi_down_gt. rewrite ltb_spec. change [|0|] with 0%Z. rewrite to_Z_sub_1_diff; auto. rewrite ltb_spec in H11. change [|1|] with 1%Z in H11. lia.
   Qed.
 
 
@@ -459,7 +459,7 @@ Proof.
   intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = false -> t = false)).
   intros b j H1 H2 H3 H4; case_eq (i == j).
   rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, andb_false_r; auto.
-  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); omega.
+  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia.
   intro H; eelim ltb_0; eassumption.
 Qed.
 
@@ -490,7 +490,7 @@ Proof.
   intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = true -> forall i, (i < j) = true -> f (a .[ i]) = true)).
   intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq.
   rewrite Int63Properties.eqb_spec in Heq; subst j; auto.
-  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; omega.
+  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia.
   intros _ i H; eelim ltb_0; eassumption.
 Qed.
 
@@ -505,7 +505,7 @@ Proof.
   intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = true -> t = true)).
   intros b j H1 H2 H3 H4; case_eq (i == j).
   rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, orb_true_r; auto.
-  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); omega.
+  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia.
   intro H; eelim ltb_0; eassumption.
 Qed.
 
@@ -536,7 +536,7 @@ Proof.
   intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = false -> forall i, (i < j) = true -> f (a .[ i]) = false)).
   intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq.
   rewrite Int63Properties.eqb_spec in Heq; subst j; auto.
-  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; omega.
+  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia.
   intros _ i H; eelim ltb_0; eassumption.
 Qed.
 
@@ -566,15 +566,15 @@ Proof.
   generalize H; clear H; case_eq (length a <= 1); intro Heq2.
   unfold afold_right; rewrite Heq1, Heq2; intro H; replace (length a - 1) with 0.
   split; auto; intros i Hi; elim (ltb_0 i); auto.
-  rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; assert ([|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; omega.
+  rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; assert ([|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; lia.
   pose (P j k := k = false -> (forall i : int, (j <= i) = true -> (i < length a - 1) = true -> f (a .[ i]) = true) /\ f (a .[ length a - 1]) = false); assert (H: P 0 (afold_right bool A true implb f a)).
   generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
   intros b i H1 H2 H3; case_eq b; intro Heq3.
   rewrite Heq3 in H3; generalize H3; case (f (a .[ i])); discriminate.
   destruct (H2 Heq3) as [H4 H5]; split; auto; intros j H6 H7; case_eq (i == j); intro Heq4.
   rewrite eqb_spec in Heq4; subst j b; generalize H3; case (f (a .[ i])); auto; discriminate.
-  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq4; assert ([|i|] <> [|j|]) by (intro H; apply Heq4, to_Z_inj; auto); omega.
-  intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega.
+  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq4; assert ([|i|] <> [|j|]) by (intro H; apply Heq4, to_Z_inj; auto); lia.
+  intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia.
   unfold P in H; intro H1; destruct (H H1) as [H2 H3]; split; auto; intro i; apply H2, leb_0.
 Qed.
 
@@ -586,7 +586,7 @@ Proof.
   intros A a f; case_eq (length a == 0); intro Heq1.
   intros _; unfold afold_right; rewrite Heq1; auto.
   case_eq (length a <= 1); intro Heq2.
-  intros [i [Hi _]]; elim (ltb_0 i); replace 0 with (length a - 1); auto; rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; assert (H1: [|length a|] <> 0%Z) by (intro H; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; change [|1|] with 1%Z in Heq2; omega.
+  intros [i [Hi _]]; elim (ltb_0 i); replace 0 with (length a - 1); auto; rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; assert (H1: [|length a|] <> 0%Z) by (intro H; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; change [|1|] with 1%Z in Heq2; lia.
   pose (P j k := (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) -> k = true); assert (H: P 0 (afold_right bool A true implb f a)).
   generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
   intros b i H1 H2 [j [H3 [H4 H5]]]; case_eq (i == j); intro Heq3.
@@ -594,9 +594,9 @@ Proof.
   rewrite H2.
   case (f (a .[ i])); auto.
   exists j; repeat split; auto; assert (H: i < j = true).
-  rewrite ltb_spec; rewrite leb_spec in H3; rewrite eqb_false_spec in Heq3; assert (H: [|i|] <> [|j|]) by (intro H; apply Heq3, to_Z_inj; auto); omega.
-  rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; omega.
-  intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega.
+  rewrite ltb_spec; rewrite leb_spec in H3; rewrite eqb_false_spec in Heq3; assert (H: [|i|] <> [|j|]) by (intro H; apply Heq3, to_Z_inj; auto); lia.
+  rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; lia.
+  intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia.
   unfold P in H; intros [i Hi]; apply H; exists i; split; auto; apply leb_0.
 Qed.
 
@@ -614,7 +614,7 @@ Proof.
   apply afold_right_ind_nonempty.
   intros b i H2 H3; subst b; case (f (a .[ i])); auto.
   apply not_0_ltb; intro H; rewrite H in Heq; discriminate.
-  apply H1; rewrite ltb_spec, to_Z_sub_1_diff; [omega| ]; intro H; rewrite H in Heq; discriminate.
+  apply H1; rewrite ltb_spec, to_Z_sub_1_diff; [lia| ]; intro H; rewrite H in Heq; discriminate.
 Qed.
 
 
@@ -626,19 +626,19 @@ Proof.
   intros A a f; case_eq (length a == 0); intro Heq1.
   intros _; left; rewrite eqb_spec in Heq1; auto.
   case_eq (length a <= 1); intro Heq2.
-  unfold afold_right; rewrite Heq1, Heq2; intro H; right; right; intros i Hi; replace i with 0; auto; apply to_Z_inj; rewrite ltb_spec in Hi; rewrite eqb_false_spec in Heq1; assert (H1: [|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; generalize (leb_0 (length a)) (leb_0 i); rewrite !leb_spec; change [|0|] with 0%Z;  omega.
+  unfold afold_right; rewrite Heq1, Heq2; intro H; right; right; intros i Hi; replace i with 0; auto; apply to_Z_inj; rewrite ltb_spec in Hi; rewrite eqb_false_spec in Heq1; assert (H1: [|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; generalize (leb_0 (length a)) (leb_0 i); rewrite !leb_spec; change [|0|] with 0%Z;  lia.
   pose (P j k := k = true -> (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) \/ (forall i : int, (j <= i) = true -> (i < length a) = true -> f (a .[ i]) = true)); assert (H: P 0 (afold_right bool A true implb f a)).
   generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
   intros b i H1 H2 H3; case_eq b; intro Heq3.
   destruct (H2 Heq3) as [[j [H4 [H5 H6]]]|H4].
-  left; exists j; repeat split; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1) in H4; omega.
+  left; exists j; repeat split; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1) in H4; lia.
   case_eq (f (a.[i])); intro Heq4.
   right; intros j H5 H6; case_eq (i == j); intro Heq5.
   rewrite eqb_spec in Heq5; subst j; auto.
-  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq5; assert ([|i|] <> [|j|]) by (intro H; apply Heq5, to_Z_inj; auto); omega.
+  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq5; assert ([|i|] <> [|j|]) by (intro H; apply Heq5, to_Z_inj; auto); lia.
   left; exists i; repeat split; auto; apply leb_refl.
   rewrite Heq3 in H3; case_eq (f (a .[ i])); intro Heq4; rewrite Heq4 in H3; try discriminate; left; exists i; repeat split; auto; apply leb_refl.
-  intros H1; right; intros i H2 H3; replace i with (length a - 1); auto; apply to_Z_inj; rewrite leb_spec in H2; rewrite (to_Z_sub_1 _ _ H3) in *; rewrite ltb_spec in H3; omega.
+  intros H1; right; intros i H2 H3; replace i with (length a - 1); auto; apply to_Z_inj; rewrite leb_spec in H2; rewrite (to_Z_sub_1 _ _ H3) in *; rewrite ltb_spec in H3; lia.
   unfold P in H; intro H1; right; destruct (H H1) as [[i [_ H2]]|H2].
   left; exists i; auto.
   right; intro i; apply H2, leb_0.
@@ -946,14 +946,14 @@ Lemma existsb_false_spec : forall f from to,
   forall i, ((from <= i) = true /\ (i <= to) = true) -> f i = false.
 Proof.
   unfold existsb;intros; setoid_rewrite leb_spec; apply foldi_cont_ZInd.
-  intros z Hz; split; auto; intros _ i [H1 H2]; assert (H3 := Z.le_trans _ _ _ H1 H2); elimtype False; omega.
+  intros z Hz; split; auto; intros _ i [H1 H2]; assert (H3 := Z.le_trans _ _ _ H1 H2); elimtype False; lia.
   intros i cont H1 H2 H3; case_eq (f i); intro Heq.
-  split; try discriminate; intro H; rewrite <- Heq; apply H; split; try omega; rewrite leb_spec in H2; auto.
+  split; try discriminate; intro H; rewrite <- Heq; apply H; split; try lia; rewrite leb_spec in H2; auto.
   rewrite H3; split; intros H j [Hj1 Hj2].
   case_eq (i == j); intro Heq2.
   rewrite eqb_spec in Heq2; subst j; auto.
-  apply H; split; auto; rewrite eqb_false_spec in Heq2; assert ([|i|] <> [|j|]) by (intro; apply Heq2, to_Z_inj; auto); omega.
-  apply H; omega.
+  apply H; split; auto; rewrite eqb_false_spec in Heq2; assert ([|i|] <> [|j|]) by (intro; apply Heq2, to_Z_inj; auto); lia.
+  apply H; lia.
 Qed.
 
 
@@ -964,8 +964,8 @@ Proof.
   unfold existsbi;intros A f t; destruct (reflect_eqb 0 (length t)).
   split; auto. intros _ i Hi. elim (ltb_0 i). rewrite e. auto.
   rewrite existsb_false_spec. split.
-  intros H i Hi. apply H. split; [apply leb_0| ]. rewrite leb_spec. rewrite (to_Z_sub_1 _ _ Hi). rewrite ltb_spec in Hi. omega.
-  intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; omega.
+  intros H i Hi. apply H. split; [apply leb_0| ]. rewrite leb_spec. rewrite (to_Z_sub_1 _ _ Hi). rewrite ltb_spec in Hi. lia.
+  intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; lia.
 Qed.
 
 
@@ -976,8 +976,8 @@ Proof.
   intros A f t; unfold PArray.existsb; case_eq (0 == length t).
   rewrite eqb_spec; intro H; split; auto; intros _ i Hi; elim (ltb_0 i); rewrite H; auto.
   intro H; rewrite existsb_false_spec; split.
-  intros H1 i Hi; apply H1; split; [apply leb_0| ]; rewrite leb_spec, (to_Z_sub_1 _ _ Hi); rewrite ltb_spec in Hi; omega.
-  intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [omega| ]; intro H3; rewrite H3 in H; discriminate.
+  intros H1 i Hi; apply H1; split; [apply leb_0| ]; rewrite leb_spec, (to_Z_sub_1 _ _ Hi); rewrite ltb_spec in Hi; lia.
+  intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [lia| ]; intro H3; rewrite H3 in H; discriminate.
 Qed.
 
 
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index c627bc2..169c761 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -416,7 +416,7 @@ Module Typ.
         | Tindex i => eqb_of_compdec (t_i.[i]).(te_compdec)
         | TZ => Z.eqb (* Zeq_bool *)
         | Tbool => Bool.eqb
-        | Tpositive => Peqb
+        | Tpositive => Pos.eqb
         | TBV n => (@BITVECTOR_LIST.bv_eq n)
         | TFArray ti te => i_eqb (TFArray ti te)
         end.
@@ -1513,7 +1513,7 @@ Qed.
         | UO_xI   => apply_unop Typ.Tpositive Typ.Tpositive xI
         | UO_Zpos => apply_unop Typ.Tpositive Typ.TZ Zpos
         | UO_Zneg => apply_unop Typ.Tpositive Typ.TZ Zneg
-        | UO_Zopp => apply_unop Typ.TZ Typ.TZ Zopp
+        | UO_Zopp => apply_unop Typ.TZ Typ.TZ Z.opp
         | UO_BVbitOf s n => apply_unop (Typ.TBV s) Typ.Tbool (BITVECTOR_LIST.bitOf n)
         | UO_BVnot s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_not s)
         | UO_BVneg s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_neg s)
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index dd1a65f..3a982b2 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -10,8 +10,8 @@
 (**************************************************************************)
 
 
-Require Import Bool List Int63 PArray SMT_classes.
-Require Import Misc State SMT_terms FArray.
+Require Import Bool List Int63 PArray Psatz.
+Require Import Misc State SMT_terms FArray SMT_classes.
 
 Import Form.
 Import Atom.
@@ -897,8 +897,6 @@ Section certif.
     afold_left bool int false orb (Lit.interp rho) a =
     C.interp rho (to_list a).
 
-  Require Import Psatz.
-
   Lemma valid_check_ext lres : C.valid rho (check_ext lres).
     unfold check_ext, eq_sel_sym.
     case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
diff --git a/src/array/FArray.v b/src/array/FArray.v
index 1f8c6b4..a17817f 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -11,7 +11,8 @@
 
 
 Require Import Bool OrderedType SMT_classes.
-Require Import ProofIrrelevance. (* TODO: REMOVE THIS AXIOM *)
+Require Import ProofIrrelevance Classical_Pred_Type ClassicalEpsilon. (* TODO: REMOVE ALL THESE AXIOMS *)
+
 
 (** 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
@@ -1777,8 +1778,6 @@ Section FArray.
 
   Section Classical_extensionnality.
 
-    Require Import Classical_Pred_Type ClassicalEpsilon.
-
     Lemma extensionnality2 : forall a b, a <> b -> (exists i, select a i <> select b i).
     Proof.
       intros.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index d6180a0..55e689d 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -10,9 +10,9 @@
 (**************************************************************************)
 
 
-Require Import Bool OrderedType BinPos ZArith.
+Require Import Bool OrderedType BinPos ZArith OrderedTypeEx.
 Require Import Int63.
-Require Import State BVList.
+Require Import State BVList FArray.
 Require Structures.
 Require Export SMT_classes.
 
@@ -119,8 +119,6 @@ End Bool.
 
 Section Z.
 
-  Require Import OrderedTypeEx.
-
   Instance Z_ord : OrdType Z.
   Proof.
     exists Z_as_OT.lt.
@@ -252,8 +250,6 @@ End Z.
 
 Section Nat.
 
-  Require Import OrderedTypeEx.
-
   Instance Nat_ord : OrdType nat.
   Proof.
     
@@ -291,9 +287,6 @@ End Nat.
 
 Section Positive.
 
-  
-  Require Import OrderedTypeEx.
-
   Instance Positive_ord : OrdType positive.
   Proof.
     exists Positive_as_OT.lt.
@@ -412,8 +405,6 @@ End BV.
 
 Section FArray.
 
-  Require Import FArray.
-  
   Instance FArray_ord key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index 8c5a597..c214c3b 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -74,7 +74,7 @@ Section certif.
     match l with
     | nil => None
     | h' :: l =>
-      let p := Ppred p in
+      let p := Pos.pred p in
       if Atom.eqb h h' then Some p else find_var_aux h p l
     end.
 
@@ -82,7 +82,7 @@ Section certif.
     let (count,map) := vm in
     match find_var_aux h count map with
     | Some p => (vm, p)
-    | None => ((Psucc count,h::map), count)
+    | None => ((Pos.succ count,h::map), count)
     end.
 
   Definition empty_vmap : vmap := (1%positive, nil).
@@ -508,7 +508,7 @@ Section certif.
       intros pvm Heq1 Heq.
       assert (1 < pvm)%positive.
        rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega.
-      assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat.
+      assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat.
        rewrite Ppred_minus, Pminus_minus;trivial.
        change (nat_of_P 1) with 1%nat ;try omega.
       revert Heq1.
@@ -554,7 +554,7 @@ Section certif.
      intros pvm p Heq1 Heq.
      assert (1 < pvm)%positive.
        rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega.
-     assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat.
+     assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat.
      rewrite Ppred_minus, Pminus_minus;trivial.
      change (nat_of_P 1) with 1%nat ;try omega.
      revert Heq1.
@@ -562,8 +562,8 @@ Section certif.
      intros Heq1;inversion Heq1;clear Heq1;subst.
      unfold is_true;rewrite andb_true_iff;intros (H1,H2).
      assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial).
-     assert (W:=nat_of_P_pos (Ppred pvm)).
-     assert (nat_of_P (pvm - Ppred pvm) - 1 = 0)%nat.
+     assert (W:=nat_of_P_pos (Pos.pred pvm)).
+     assert (nat_of_P (pvm - Pos.pred pvm) - 1 = 0)%nat.
       rewrite Pminus_minus;try omega.
       apply Plt_lt;omega.
      rewrite H4;simpl.
@@ -571,10 +571,10 @@ Section certif.
      rewrite Hz;trivial.
      unfold is_true;rewrite andb_true_iff;intros Heq1 (H1,H2).
      assert (W:= find_var_aux_lt _ _ _ _ Heq1 H0).
-     assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Ppred pvm - p) - 1))%nat.
+     assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Pos.pred pvm - p) - 1))%nat.
        assert (W1:= W);rewrite <- Plt_lt in W.
        rewrite !Pminus_minus;trivial.
-       assert (W2:=nat_of_P_pos (Ppred pvm)).
+       assert (W2:=nat_of_P_pos (Pos.pred pvm)).
        omega.
        rewrite Plt_lt.
        apply lt_trans with (1:= W1);omega.
@@ -585,7 +585,7 @@ Section certif.
      rewrite Hh;trivial.
      rewrite Psucc_S;omega.
      intros p Hlt;
-      assert (nat_of_P (Psucc pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat.
+      assert (nat_of_P (Pos.succ pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat.
        assert (W1:= Hlt);rewrite <- Plt_lt in W1.
        rewrite !Pminus_minus;trivial.
        rewrite Psucc_S;omega.
@@ -595,7 +595,7 @@ Section certif.
      rewrite Zpos_succ_morphism;omega.
      destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz).
      rewrite Hz;unfold interp_vmap;simpl.
-     assert (nat_of_P (Psucc pvm - pvm) = 1%nat).
+     assert (nat_of_P (Pos.succ pvm - pvm) = 1%nat).
        rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus.
        change (nat_of_P 1) with 1%nat;omega.
        rewrite Plt_lt, Pplus_plus.
@@ -611,7 +611,7 @@ Section certif.
    Proof.
     unfold is_true;induction pe;simpl;trivial.
     rewrite <- !Zlt_is_lt_bool; rewrite <- Ple_le in H.
-    intros H1;apply Zlt_le_trans with (1:= H1);trivial.
+    intros H1;apply Z.lt_le_trans with (1:= H1);trivial.
     rewrite !andb_true_iff;intros (H1,H2);auto.
     rewrite !andb_true_iff;intros (H1,H2);auto.
     rewrite !andb_true_iff;intros (H1,H2);auto.
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 203077b..64f0b20 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -98,10 +98,10 @@ let rec sort_of_sort = function
 
 let declare_sort rt sym =
   let s = string_of_symbol sym in
-  let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in
+  let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in
   let compdec_type = mklApp cCompDec [| cons_t |] in
   let compdec_var =
-    declare_new_variable (Names.id_of_string ("CompDec_"^s)) compdec_type in
+    Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in
   let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in
   let res = SmtBtype.declare rt cons_t ce in
   VeritSyntax.add_btype s res;
@@ -115,7 +115,7 @@ let declare_fun rt ro sym arg cod =
   let coqTy = List.fold_right (fun typ c ->
       Term.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
-  let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
+  let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
   VeritSyntax.add_fun s op;
   op
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 895d217..ad5ec1d 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -11,6 +11,7 @@
 
 
 open Coqlib
+open SmtMisc
 
 
 let gen_constant = Structures.gen_constant
@@ -274,7 +275,7 @@ let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "i
 let make_certif_ops modules args =
   let gen_constant c =
     match args with
-      | Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args)
+      | Some args -> lazy (mklApp (gen_constant modules c) args)
       | None -> gen_constant modules c in
  (gen_constant "step",
   gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten",
@@ -300,14 +301,14 @@ let make_certif_ops modules args =
 (** Useful constructions *)
 
 let ceq_refl_true =
-  lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
+  lazy (mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
 
 let eq_refl_true () = Lazy.force ceq_refl_true
 
 let vm_cast_true_no_check t =
-  Term.mkCast(eq_refl_true (),
-              Term.VMcast,
-              SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
+  Structures.mkCast(eq_refl_true (),
+              Structures.vmcast,
+              mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
 
 (* This version checks convertibility right away instead of delaying it at
    Qed. This allows to report issues to the user as soon as he/she runs one of
@@ -315,9 +316,9 @@ let vm_cast_true_no_check t =
 let vm_cast_true env t =
   try
     Structures.vm_conv Reduction.CUMUL env
-      (SmtMisc.mklApp ceq
+      (mklApp ceq
          [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|])
-      (SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]);
+      (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]);
     vm_cast_true_no_check t
   with Reduction.NotConvertible ->
     Structures.error ("SMTCoq was not able to check the proof certificate.")
@@ -326,19 +327,19 @@ let vm_cast_true env t =
 (* Compute a nat *)
 let rec mkNat = function
   | 0 -> Lazy.force cO
-  | i -> SmtMisc.mklApp cS [|mkNat (i-1)|]
+  | i -> mklApp cS [|mkNat (i-1)|]
 
 (* Compute a positive *)
 let rec mkPositive = function
   | 1 -> Lazy.force cxH
   | i ->
      let c = if (i mod 2) = 0 then cxO else cxI in
-     SmtMisc.mklApp c [|mkPositive (i / 2)|]
+     mklApp c [|mkPositive (i / 2)|]
 
 (* Compute a N *)
 let mkN = function
   | 0 -> Lazy.force cN0
-  | i -> SmtMisc.mklApp cNpos [|mkPositive i|]
+  | i -> mklApp cNpos [|mkPositive i|]
 
 (* Compute a Boolean *)
 let mkBool = function
@@ -347,47 +348,47 @@ let mkBool = function
 
 (* Compute a Boolean list *)
 let rec mk_bv_list = function
-  | [] -> SmtMisc.mklApp cnil [|Lazy.force cbool|]
+  | [] -> mklApp cnil [|Lazy.force cbool|]
   | b :: bv ->
-    SmtMisc.mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
+    mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
 
 
 (* Reification *)
 
 let mk_bool b =
-  let c, args = Term.decompose_app b in
-  if Term.eq_constr c (Lazy.force ctrue) then true
-  else if Term.eq_constr c (Lazy.force cfalse) then false
+  let c, args = Structures.decompose_app b in
+  if Structures.eq_constr c (Lazy.force ctrue) then true
+  else if Structures.eq_constr c (Lazy.force cfalse) then false
   else assert false
 
 let rec mk_bool_list bs =
-  let c, args = Term.decompose_app bs in
-  if Term.eq_constr c (Lazy.force cnil) then []
-  else if Term.eq_constr c (Lazy.force ccons) then
+  let c, args = Structures.decompose_app bs in
+  if Structures.eq_constr c (Lazy.force cnil) then []
+  else if Structures.eq_constr c (Lazy.force ccons) then
     match args with
     | [_; b; bs] -> mk_bool b :: mk_bool_list bs
     | _ -> assert false
   else assert false
 
 let rec mk_nat n =
-  let c, args = Term.decompose_app n in
-  if Term.eq_constr c (Lazy.force cO) then
+  let c, args = Structures.decompose_app n in
+  if Structures.eq_constr c (Lazy.force cO) then
     0
-  else if Term.eq_constr c (Lazy.force cS) then
+  else if Structures.eq_constr c (Lazy.force cS) then
     match args with
     | [n] -> (mk_nat n) + 1
     | _ -> assert false
   else assert false
 
 let rec mk_positive n =
-  let c, args = Term.decompose_app n in
-  if Term.eq_constr c (Lazy.force cxH) then
+  let c, args = Structures.decompose_app n in
+  if Structures.eq_constr c (Lazy.force cxH) then
     1
-  else if Term.eq_constr c (Lazy.force cxO) then
+  else if Structures.eq_constr c (Lazy.force cxO) then
     match args with
     | [n] -> 2 * (mk_positive n)
     | _ -> assert false
-  else if Term.eq_constr c (Lazy.force cxI) then
+  else if Structures.eq_constr c (Lazy.force cxI) then
     match args with
     | [n] -> 2 * (mk_positive n) + 1
     | _ -> assert false
@@ -395,10 +396,10 @@ let rec mk_positive n =
 
 
 let mk_N n =
-  let c, args = Term.decompose_app n in
-  if Term.eq_constr c (Lazy.force cN0) then
+  let c, args = Structures.decompose_app n in
+  if Structures.eq_constr c (Lazy.force cN0) then
     0
-  else if Term.eq_constr c (Lazy.force cNpos) then
+  else if Structures.eq_constr c (Lazy.force cNpos) then
     match args with
     | [n] -> mk_positive n
     | _ -> assert false
@@ -406,13 +407,13 @@ let mk_N n =
 
 
 let mk_Z n =
-  let c, args = Term.decompose_app n in
-  if Term.eq_constr c (Lazy.force cZ0) then 0
-  else if Term.eq_constr c (Lazy.force cZpos) then
+  let c, args = Structures.decompose_app n in
+  if Structures.eq_constr c (Lazy.force cZ0) then 0
+  else if Structures.eq_constr c (Lazy.force cZpos) then
     match args with
     | [n] -> mk_positive n
     | _ -> assert false
-  else if Term.eq_constr c (Lazy.force cZneg) then
+  else if Structures.eq_constr c (Lazy.force cZneg) then
     match args with
     | [n] -> - mk_positive n
     | _ -> assert false
@@ -421,12 +422,12 @@ let mk_Z n =
 
 (* size of bivectors are either N.of_nat (length l) or an N *)
 let mk_bvsize n =
-  let c, args = Term.decompose_app n in
-  if Term.eq_constr c (Lazy.force cof_nat) then
+  let c, args = Structures.decompose_app n in
+  if Structures.eq_constr c (Lazy.force cof_nat) then
     match args with
     | [nl] ->
-      let c, args = Term.decompose_app nl in
-      if Term.eq_constr c (Lazy.force clength) then
+      let c, args = Structures.decompose_app nl in
+      if Structures.eq_constr c (Lazy.force clength) then
         match args with
         | [_; l] -> List.length (mk_bool_list l)
         | _ -> assert false
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 9aeddac..bf626b3 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -10,254 +10,254 @@
 (**************************************************************************)
 
 
-val gen_constant : string list list -> string -> Term.constr lazy_t
+val gen_constant : string list list -> string -> Structures.constr lazy_t
 
 (* Int63 *)
-val cint : Term.constr lazy_t
-val ceq63 : Term.constr lazy_t
+val cint : Structures.constr lazy_t
+val ceq63 : Structures.constr lazy_t
 
 (* PArray *)
-val carray : Term.constr lazy_t
+val carray : Structures.constr lazy_t
 
 (* nat *)
-val cnat : Term.constr lazy_t
-val cO : Term.constr lazy_t
-val cS : Term.constr lazy_t
+val cnat : Structures.constr lazy_t
+val cO : Structures.constr lazy_t
+val cS : Structures.constr lazy_t
 
 (* Positive *)
-val cpositive : Term.constr lazy_t
-val cxI : Term.constr lazy_t
-val cxO : Term.constr lazy_t
-val cxH : Term.constr lazy_t
-val ceqbP : Term.constr lazy_t
+val cpositive : Structures.constr lazy_t
+val cxI : Structures.constr lazy_t
+val cxO : Structures.constr lazy_t
+val cxH : Structures.constr lazy_t
+val ceqbP : Structures.constr lazy_t
 
 (* N *)
-val cN : Term.constr lazy_t
-val cN0 : Term.constr lazy_t
-val cNpos : Term.constr lazy_t
-val cof_nat : Term.constr lazy_t
+val cN : Structures.constr lazy_t
+val cN0 : Structures.constr lazy_t
+val cNpos : Structures.constr lazy_t
+val cof_nat : Structures.constr lazy_t
 
 (* Z *)
-val cZ : Term.constr lazy_t
-val cZ0 : Term.constr lazy_t
-val cZpos : Term.constr lazy_t
-val cZneg : Term.constr lazy_t
-val copp : Term.constr lazy_t
-val cadd : Term.constr lazy_t
-val csub : Term.constr lazy_t
-val cmul : Term.constr lazy_t
-val cltb : Term.constr lazy_t
-val cleb : Term.constr lazy_t
-val cgeb : Term.constr lazy_t
-val cgtb : Term.constr lazy_t
-val ceqbZ : Term.constr lazy_t
+val cZ : Structures.constr lazy_t
+val cZ0 : Structures.constr lazy_t
+val cZpos : Structures.constr lazy_t
+val cZneg : Structures.constr lazy_t
+val copp : Structures.constr lazy_t
+val cadd : Structures.constr lazy_t
+val csub : Structures.constr lazy_t
+val cmul : Structures.constr lazy_t
+val cltb : Structures.constr lazy_t
+val cleb : Structures.constr lazy_t
+val cgeb : Structures.constr lazy_t
+val cgtb : Structures.constr lazy_t
+val ceqbZ : Structures.constr lazy_t
 
 (* Booleans *)
-val cbool : Term.constr lazy_t
-val ctrue : Term.constr lazy_t
-val cfalse : Term.constr lazy_t
-val candb : Term.constr lazy_t
-val corb : Term.constr lazy_t
-val cxorb : Term.constr lazy_t
-val cnegb : Term.constr lazy_t
-val cimplb : Term.constr lazy_t
-val ceqb : Term.constr lazy_t
-val cifb : Term.constr lazy_t
-val ciff : Term.constr lazy_t
-val creflect : Term.constr lazy_t
+val cbool : Structures.constr lazy_t
+val ctrue : Structures.constr lazy_t
+val cfalse : Structures.constr lazy_t
+val candb : Structures.constr lazy_t
+val corb : Structures.constr lazy_t
+val cxorb : Structures.constr lazy_t
+val cnegb : Structures.constr lazy_t
+val cimplb : Structures.constr lazy_t
+val ceqb : Structures.constr lazy_t
+val cifb : Structures.constr lazy_t
+val ciff : Structures.constr lazy_t
+val creflect : Structures.constr lazy_t
 
 (* Lists *)
-val clist : Term.constr lazy_t
-val cnil : Term.constr lazy_t
-val ccons : Term.constr lazy_t
-val clength : Term.constr lazy_t
+val clist : Structures.constr lazy_t
+val cnil : Structures.constr lazy_t
+val ccons : Structures.constr lazy_t
+val clength : Structures.constr lazy_t
 
 (* Option *)
-val coption : Term.constr lazy_t
-val cSome : Term.constr lazy_t
-val cNone : Term.constr lazy_t
+val coption : Structures.constr lazy_t
+val cSome : Structures.constr lazy_t
+val cNone : Structures.constr lazy_t
 
 (* Pairs *)
-val cpair : Term.constr lazy_t
-val cprod : Term.constr lazy_t
+val cpair : Structures.constr lazy_t
+val cprod : Structures.constr lazy_t
 
 (* Dependent pairs *)
-val csigT : Term.constr lazy_t
+val csigT : Structures.constr lazy_t
 
 (* Logical Operators *)
-val cnot : Term.constr lazy_t
-val ceq : Term.constr lazy_t
-val crefl_equal : Term.constr lazy_t
-val cconj : Term.constr lazy_t
-val cand : Term.constr lazy_t
+val cnot : Structures.constr lazy_t
+val ceq : Structures.constr lazy_t
+val crefl_equal : Structures.constr lazy_t
+val cconj : Structures.constr lazy_t
+val cand : Structures.constr lazy_t
 
 (* Bit vectors *)
-val cbitvector : Term.constr lazy_t
-val cof_bits : Term.constr lazy_t
-val cbitOf : Term.constr lazy_t
-val cbv_eq : Term.constr lazy_t
-val cbv_not : Term.constr lazy_t
-val cbv_neg : Term.constr lazy_t
-val cbv_and : Term.constr lazy_t
-val cbv_or : Term.constr lazy_t
-val cbv_xor : Term.constr lazy_t
-val cbv_add : Term.constr lazy_t
-val cbv_mult : Term.constr lazy_t
-val cbv_ult : Term.constr lazy_t
-val cbv_slt : Term.constr lazy_t
-val cbv_concat : Term.constr lazy_t
-val cbv_extr : Term.constr lazy_t
-val cbv_zextn : Term.constr lazy_t
-val cbv_sextn : Term.constr lazy_t
-val cbv_shl : Term.constr lazy_t
-val cbv_shr : Term.constr lazy_t
+val cbitvector : Structures.constr lazy_t
+val cof_bits : Structures.constr lazy_t
+val cbitOf : Structures.constr lazy_t
+val cbv_eq : Structures.constr lazy_t
+val cbv_not : Structures.constr lazy_t
+val cbv_neg : Structures.constr lazy_t
+val cbv_and : Structures.constr lazy_t
+val cbv_or : Structures.constr lazy_t
+val cbv_xor : Structures.constr lazy_t
+val cbv_add : Structures.constr lazy_t
+val cbv_mult : Structures.constr lazy_t
+val cbv_ult : Structures.constr lazy_t
+val cbv_slt : Structures.constr lazy_t
+val cbv_concat : Structures.constr lazy_t
+val cbv_extr : Structures.constr lazy_t
+val cbv_zextn : Structures.constr lazy_t
+val cbv_sextn : Structures.constr lazy_t
+val cbv_shl : Structures.constr lazy_t
+val cbv_shr : Structures.constr lazy_t
 
 (* Arrays *)
-val cfarray : Term.constr lazy_t
-val cselect : Term.constr lazy_t
-val cstore : Term.constr lazy_t
-val cdiff : Term.constr lazy_t
-val cequalarray : Term.constr lazy_t
+val cfarray : Structures.constr lazy_t
+val cselect : Structures.constr lazy_t
+val cstore : Structures.constr lazy_t
+val cdiff : Structures.constr lazy_t
+val cequalarray : Structures.constr lazy_t
 
 (* OrderedType *)
 
 (* SMT_terms *)
-val cState_C_t : Term.constr lazy_t
-val cState_S_t : Term.constr lazy_t
-
-val cdistinct : Term.constr lazy_t
-
-val ctype : Term.constr lazy_t
-val cTZ : Term.constr lazy_t
-val cTbool : Term.constr lazy_t
-val cTpositive : Term.constr lazy_t
-val cTBV : Term.constr lazy_t
-val cTFArray : Term.constr lazy_t
-val cTindex : Term.constr lazy_t
-
-val cinterp_t : Term.constr lazy_t
-val cdec_interp : Term.constr lazy_t
-val cord_interp : Term.constr lazy_t
-val ccomp_interp : Term.constr lazy_t
-val cinh_interp : Term.constr lazy_t
-
-val cinterp_eqb : Term.constr lazy_t
-
-val ctyp_compdec : Term.constr lazy_t
-val cTyp_compdec : Term.constr lazy_t
-val cunit_typ_compdec : Term.constr lazy_t
-val cte_carrier : Term.constr lazy_t
-val cte_compdec : Term.constr lazy_t
-val ceqb_of_compdec : Term.constr lazy_t
-val cCompDec : Term.constr lazy_t
-
-val cbool_compdec : Term.constr lazy_t
-val cZ_compdec : Term.constr lazy_t
-val cPositive_compdec : Term.constr lazy_t
-val cBV_compdec : Term.constr lazy_t
-val cFArray_compdec : Term.constr lazy_t
-
-val ctval : Term.constr lazy_t
-val cTval : Term.constr lazy_t
-
-val cCO_xH : Term.constr lazy_t
-val cCO_Z0 : Term.constr lazy_t
-val cCO_BV : Term.constr lazy_t
-
-val cUO_xO : Term.constr lazy_t
-val cUO_xI : Term.constr lazy_t
-val cUO_Zpos : Term.constr lazy_t
-val cUO_Zneg : Term.constr lazy_t
-val cUO_Zopp : Term.constr lazy_t
-val cUO_BVbitOf : Term.constr lazy_t
-val cUO_BVnot : Term.constr lazy_t
-val cUO_BVneg : Term.constr lazy_t
-val cUO_BVextr : Term.constr lazy_t
-val cUO_BVzextn : Term.constr lazy_t
-val cUO_BVsextn : Term.constr lazy_t
-
-val cBO_Zplus : Term.constr lazy_t
-val cBO_Zminus : Term.constr lazy_t
-val cBO_Zmult : Term.constr lazy_t
-val cBO_Zlt : Term.constr lazy_t
-val cBO_Zle : Term.constr lazy_t
-val cBO_Zge : Term.constr lazy_t
-val cBO_Zgt : Term.constr lazy_t
-val cBO_eq : Term.constr lazy_t
-val cBO_BVand : Term.constr lazy_t
-val cBO_BVor : Term.constr lazy_t
-val cBO_BVxor : Term.constr lazy_t
-val cBO_BVadd : Term.constr lazy_t
-val cBO_BVmult : Term.constr lazy_t
-val cBO_BVult : Term.constr lazy_t
-val cBO_BVslt : Term.constr lazy_t
-val cBO_BVconcat : Term.constr lazy_t
-val cBO_BVshl : Term.constr lazy_t
-val cBO_BVshr : Term.constr lazy_t
-val cBO_select : Term.constr lazy_t
-val cBO_diffarray : Term.constr lazy_t
-
-val cTO_store : Term.constr lazy_t
-
-val cNO_distinct : Term.constr lazy_t
-
-val catom : Term.constr lazy_t
-val cAcop : Term.constr lazy_t
-val cAuop : Term.constr lazy_t
-val cAbop : Term.constr lazy_t
-val cAtop : Term.constr lazy_t
-val cAnop : Term.constr lazy_t
-val cAapp : Term.constr lazy_t
-
-val cform : Term.constr lazy_t
-val cFatom : Term.constr lazy_t
-val cFtrue : Term.constr lazy_t
-val cFfalse : Term.constr lazy_t
-val cFnot2 : Term.constr lazy_t
-val cFand : Term.constr lazy_t
-val cFor : Term.constr lazy_t
-val cFxor : Term.constr lazy_t
-val cFimp : Term.constr lazy_t
-val cFiff : Term.constr lazy_t
-val cFite : Term.constr lazy_t
-val cFbbT : Term.constr lazy_t
-
-val cis_true : Term.constr lazy_t
-
-val cvalid_sat_checker : Term.constr lazy_t
-val cinterp_var_sat_checker : Term.constr lazy_t
+val cState_C_t : Structures.constr lazy_t
+val cState_S_t : Structures.constr lazy_t
+
+val cdistinct : Structures.constr lazy_t
+
+val ctype : Structures.constr lazy_t
+val cTZ : Structures.constr lazy_t
+val cTbool : Structures.constr lazy_t
+val cTpositive : Structures.constr lazy_t
+val cTBV : Structures.constr lazy_t
+val cTFArray : Structures.constr lazy_t
+val cTindex : Structures.constr lazy_t
+
+val cinterp_t : Structures.constr lazy_t
+val cdec_interp : Structures.constr lazy_t
+val cord_interp : Structures.constr lazy_t
+val ccomp_interp : Structures.constr lazy_t
+val cinh_interp : Structures.constr lazy_t
+
+val cinterp_eqb : Structures.constr lazy_t
+
+val ctyp_compdec : Structures.constr lazy_t
+val cTyp_compdec : Structures.constr lazy_t
+val cunit_typ_compdec : Structures.constr lazy_t
+val cte_carrier : Structures.constr lazy_t
+val cte_compdec : Structures.constr lazy_t
+val ceqb_of_compdec : Structures.constr lazy_t
+val cCompDec : Structures.constr lazy_t
+
+val cbool_compdec : Structures.constr lazy_t
+val cZ_compdec : Structures.constr lazy_t
+val cPositive_compdec : Structures.constr lazy_t
+val cBV_compdec : Structures.constr lazy_t
+val cFArray_compdec : Structures.constr lazy_t
+
+val ctval : Structures.constr lazy_t
+val cTval : Structures.constr lazy_t
+
+val cCO_xH : Structures.constr lazy_t
+val cCO_Z0 : Structures.constr lazy_t
+val cCO_BV : Structures.constr lazy_t
+
+val cUO_xO : Structures.constr lazy_t
+val cUO_xI : Structures.constr lazy_t
+val cUO_Zpos : Structures.constr lazy_t
+val cUO_Zneg : Structures.constr lazy_t
+val cUO_Zopp : Structures.constr lazy_t
+val cUO_BVbitOf : Structures.constr lazy_t
+val cUO_BVnot : Structures.constr lazy_t
+val cUO_BVneg : Structures.constr lazy_t
+val cUO_BVextr : Structures.constr lazy_t
+val cUO_BVzextn : Structures.constr lazy_t
+val cUO_BVsextn : Structures.constr lazy_t
+
+val cBO_Zplus : Structures.constr lazy_t
+val cBO_Zminus : Structures.constr lazy_t
+val cBO_Zmult : Structures.constr lazy_t
+val cBO_Zlt : Structures.constr lazy_t
+val cBO_Zle : Structures.constr lazy_t
+val cBO_Zge : Structures.constr lazy_t
+val cBO_Zgt : Structures.constr lazy_t
+val cBO_eq : Structures.constr lazy_t
+val cBO_BVand : Structures.constr lazy_t
+val cBO_BVor : Structures.constr lazy_t
+val cBO_BVxor : Structures.constr lazy_t
+val cBO_BVadd : Structures.constr lazy_t
+val cBO_BVmult : Structures.constr lazy_t
+val cBO_BVult : Structures.constr lazy_t
+val cBO_BVslt : Structures.constr lazy_t
+val cBO_BVconcat : Structures.constr lazy_t
+val cBO_BVshl : Structures.constr lazy_t
+val cBO_BVshr : Structures.constr lazy_t
+val cBO_select : Structures.constr lazy_t
+val cBO_diffarray : Structures.constr lazy_t
+
+val cTO_store : Structures.constr lazy_t
+
+val cNO_distinct : Structures.constr lazy_t
+
+val catom : Structures.constr lazy_t
+val cAcop : Structures.constr lazy_t
+val cAuop : Structures.constr lazy_t
+val cAbop : Structures.constr lazy_t
+val cAtop : Structures.constr lazy_t
+val cAnop : Structures.constr lazy_t
+val cAapp : Structures.constr lazy_t
+
+val cform : Structures.constr lazy_t
+val cFatom : Structures.constr lazy_t
+val cFtrue : Structures.constr lazy_t
+val cFfalse : Structures.constr lazy_t
+val cFnot2 : Structures.constr lazy_t
+val cFand : Structures.constr lazy_t
+val cFor : Structures.constr lazy_t
+val cFxor : Structures.constr lazy_t
+val cFimp : Structures.constr lazy_t
+val cFiff : Structures.constr lazy_t
+val cFite : Structures.constr lazy_t
+val cFbbT : Structures.constr lazy_t
+
+val cis_true : Structures.constr lazy_t
+
+val cvalid_sat_checker : Structures.constr lazy_t
+val cinterp_var_sat_checker : Structures.constr lazy_t
 
 val make_certif_ops :
            string list list ->
-           Term.constr array option ->
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-           Term.constr lazy_t * Term.constr lazy_t
+           Structures.constr array option ->
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
+           Structures.constr lazy_t * Structures.constr lazy_t
 
 (* Some constructions *)
-val ceq_refl_true : Term.constr lazy_t
-val eq_refl_true : unit -> Term.constr
-val vm_cast_true_no_check : Term.constr -> Term.constr
-val vm_cast_true : Environ.env -> Term.constr -> Term.constr
-val mkNat : int -> Term.constr
-val mkN : int -> Term.constr
-val mk_bv_list : bool list -> Term.constr
+val ceq_refl_true : Structures.constr lazy_t
+val eq_refl_true : unit -> Structures.constr
+val vm_cast_true_no_check : Structures.constr -> Structures.constr
+val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr
+val mkNat : int -> Structures.constr
+val mkN : int -> Structures.constr
+val mk_bv_list : bool list -> Structures.constr
 
 (* Reification *)
-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
+val mk_bool : Structures.constr -> bool
+val mk_bool_list : Structures.constr -> bool list
+val mk_nat : Structures.constr -> int
+val mk_N : Structures.constr -> int
+val mk_Z : Structures.constr -> int
+val mk_bvsize : Structures.constr -> int
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index 549462c..c91cee1 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -27,7 +27,7 @@ module Atom =
 
     type reify_tbl =
         { mutable count : int;
-	          tbl : (Term.constr, int) Hashtbl.t 
+	          tbl : (Structures.constr, int) Hashtbl.t
 	}
 
     let create () = 
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 4ecfae3..49bc590 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -23,13 +23,13 @@ module Atom : sig
 
   type reify_tbl = {
       mutable count : int;
-      tbl : (Term.constr, t) Hashtbl.t;
+      tbl : (Structures.constr, t) Hashtbl.t;
     }
   val create : unit -> reify_tbl
-  val declare : reify_tbl -> Term.constr -> t
-  val get : reify_tbl -> Term.constr -> t
-  val atom_tbl : reify_tbl -> Term.constr array
-  val interp_tbl : reify_tbl -> Term.constr
+  val declare : reify_tbl -> Structures.constr -> t
+  val get : reify_tbl -> Structures.constr -> t
+  val atom_tbl : reify_tbl -> Structures.constr array
+  val interp_tbl : reify_tbl -> Structures.constr
 end
 
 
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 330884b..16d9bdb 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -68,7 +68,7 @@ type nop =
 type op_def = {
     tparams : btype array;
     tres : btype;
-    op_val : Term.constr }
+    op_val : Structures.constr }
 
 type index = Index of int
            | Rel_name of string
@@ -80,14 +80,14 @@ let destruct s (i, hval) = match i with
     | Rel_name _ -> failwith s
 
 let dummy_indexed_op i dom codom =
-  (i, {tparams = dom; tres = codom; op_val = Term.mkProp})
+  (i, {tparams = dom; tres = codom; op_val = Structures.mkProp})
 
 let indexed_op_index i =
   let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
   index
 
 let debruijn_indexed_op i ty =
-  (Index i, {tparams = [||]; tres = ty; op_val = Term.mkRel i})
+  (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i})
 
 module Op =
   struct
@@ -339,7 +339,7 @@ module Op =
     (* reify table *)
     type reify_tbl =
       { mutable count : int;
-	        tbl : (Term.constr, indexed_op) Hashtbl.t
+	        tbl : (Structures.constr, indexed_op) Hashtbl.t
       }
 
     let create () =
@@ -692,7 +692,7 @@ module Atom =
         Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta;
         Format.fprintf fmt ") ( ";
         SmtBtype.to_smt fmt bt;
-        Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Printer.pr_constr t))
+        Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t))
 
       and to_smt_bop op h1 h2 =
         let s = match op with
@@ -1019,8 +1019,8 @@ module Atom =
           else CCunknown_deps (gobble_of_coq_cst cc)
         with Not_found -> CCunknown
       in
-      let rec mk_hatom (h : Term.constr) =
-        let c, args = Term.decompose_app h in
+      let rec mk_hatom (h : Structures.constr) =
+        let c, args = Structures.decompose_app h in
 	match get_cst c with
         | CCxH -> mk_cop CCxH args
         | CCZ0 -> mk_cop CCZ0 args
@@ -1248,10 +1248,10 @@ module Atom =
           with | Not_found ->
             let targs = Array.map type_of hargs in
             let tres = SmtBtype.of_coq rt known_logic ty in
-            let os = if Term.isRel c then
-                       let i = Term.destRel c in
+            let os = if Structures.isRel c then
+                       let i = Structures.destRel c in
                        let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
-                       Some (string_of_name n)
+                       Some (Structures.string_of_name n)
                      else
                        None
             in
@@ -1267,7 +1267,7 @@ module Atom =
          [gobble] *)
       and mk_unknown_deps c args ty gobble =
         let deps, args = split_list_at gobble args in
-        let c = Term.mkApp (c, Array.of_list deps) in
+        let c = Structures.mkApp (c, Array.of_list deps) in
         mk_unknown c args ty
 
       in
@@ -1320,12 +1320,12 @@ module Atom =
 	  let pc =
 	    match atom a with
               | Acop c -> Op.interp_cop c
-              | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
+              | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|])
               | Abop (op,h1,h2) ->
-                Term.mkApp (Op.interp_bop t_i op,
+                Structures.mkApp (Op.interp_bop t_i op,
                             [|interp_atom h1; interp_atom h2|])
               | Atop (op,h1,h2,h3) ->
-                Term.mkApp (Op.interp_top t_i op,
+                Structures.mkApp (Op.interp_top t_i op,
                             [|interp_atom h1; interp_atom h2; interp_atom h3|])
               | Anop (NO_distinct ty as op,ha) ->
                 let cop = Op.interp_nop t_i op in
@@ -1333,9 +1333,9 @@ module Atom =
                 let cargs = Array.fold_right (fun h l ->
                     mklApp ccons [|typ; interp_atom h; l|])
                     ha (mklApp cnil [|typ|]) in
-                Term.mkApp (cop,[|cargs|])
+                Structures.mkApp (cop,[|cargs|])
               | Aapp (op,t) ->
-                Term.mkApp ((snd op).op_val, Array.map interp_atom t) in
+                Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in
 	  Hashtbl.add atom_tbl l pc;
 	  pc in
       interp_atom a
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index a542ad6..a6a1761 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -76,14 +76,14 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Term.constr -> btype array ->
+    val declare : reify_tbl -> Structures.constr -> btype array ->
                   btype -> string option -> indexed_op
 
-    val of_coq : reify_tbl -> Term.constr -> indexed_op
+    val of_coq : reify_tbl -> Structures.constr -> indexed_op
 
-    val interp_tbl : Term.constr ->
-      (btype array -> btype -> Term.constr -> Term.constr) ->
-      reify_tbl -> Term.constr
+    val interp_tbl : Structures.constr ->
+      (btype array -> btype -> Structures.constr -> Structures.constr) ->
+      reify_tbl -> Structures.constr
 
     val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
 
@@ -143,18 +143,18 @@ module Atom :
 
       (** Given a coq term, build the corresponding atom *)
       val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
-        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Term.constr -> t
+        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
 
-      val get_coq_term_op : int -> Term.constr
+      val get_coq_term_op : int -> Structures.constr
 
-      val to_coq : t -> Term.constr
+      val to_coq : t -> Structures.constr
 
       val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
 
-      val interp_tbl : reify_tbl -> Term.constr
+      val interp_tbl : reify_tbl -> Structures.constr
 
-      val interp_to_coq : Term.constr -> (int, Term.constr) Hashtbl.t ->
-	t -> Term.constr
+      val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t ->
+	t -> Structures.constr
 
       val logic : t -> SmtMisc.logic
 
@@ -202,5 +202,5 @@ module Trace : sig
 end
 
 
-val make_t_i : SmtBtype.reify_tbl -> Term.constr
-val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr
+val make_t_i : SmtBtype.reify_tbl -> Structures.constr
+val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 119c046..948acaa 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -15,9 +15,9 @@ open CoqTerms
 
 (** Syntaxified version of Coq type *)
 
-type indexed_type = Term.constr gen_hashed
+type indexed_type = Structures.constr gen_hashed
 
-let dummy_indexed_type i = {index = i; hval = Term.mkProp}
+let dummy_indexed_type i = {index = i; hval = Structures.mkProp}
 let indexed_type_index i = i.index
 let indexed_type_hval i = i.hval
 
@@ -76,8 +76,8 @@ let rec logic = function
 (* reify table *)
 type reify_tbl =
   { mutable count : int;
-    tbl : (Term.constr, btype) Hashtbl.t;
-    mutable cuts : (Structures.names_id * Term.types) list;
+    tbl : (Structures.constr, btype) Hashtbl.t;
+    mutable cuts : (Structures.id * Structures.types) list;
     unsup_tbl : (btype, btype) Hashtbl.t;
   }
 
@@ -175,8 +175,8 @@ let rec compdec_btype reify = function
        [|interp_to_coq reify ti; interp_to_coq reify te;
          compdec_btype reify ti; compdec_btype reify te|]
   | Tindex i ->
-     let c, args = Term.decompose_app i.hval in
-     if Term.eq_constr c (Lazy.force cTyp_compdec) then
+     let c, args = Structures.decompose_app i.hval in
+     if Structures.eq_constr c (Lazy.force cTyp_compdec) then
        match args with
          | [_; tic] -> tic
          | _ -> assert false
@@ -195,22 +195,22 @@ let declare_and_compdec reify t ty =
 
 let rec of_coq reify known_logic t =
   try
-    let c, args = Term.decompose_app t in
-    if Term.eq_constr c (Lazy.force cbool) ||
-         Term.eq_constr c (Lazy.force cTbool) then Tbool
-    else if Term.eq_constr c (Lazy.force cZ) ||
-              Term.eq_constr c (Lazy.force cTZ) then
+    let c, args = Structures.decompose_app t in
+    if Structures.eq_constr c (Lazy.force cbool) ||
+         Structures.eq_constr c (Lazy.force cTbool) then Tbool
+    else if Structures.eq_constr c (Lazy.force cZ) ||
+              Structures.eq_constr c (Lazy.force cTZ) then
       check_known TZ known_logic
-    else if Term.eq_constr c (Lazy.force cpositive) ||
-              Term.eq_constr c (Lazy.force cTpositive) then
+    else if Structures.eq_constr c (Lazy.force cpositive) ||
+              Structures.eq_constr c (Lazy.force cTpositive) then
       check_known Tpositive known_logic
-    else if Term.eq_constr c (Lazy.force cbitvector) ||
-              Term.eq_constr c (Lazy.force cTBV) then
+    else if Structures.eq_constr c (Lazy.force cbitvector) ||
+              Structures.eq_constr c (Lazy.force cTBV) then
       match args with
         | [s] -> check_known (TBV (mk_bvsize s)) known_logic
         | _ -> assert false
-    else if Term.eq_constr c (Lazy.force cfarray) ||
-              Term.eq_constr c (Lazy.force cTFArray) then
+    else if Structures.eq_constr c (Lazy.force cfarray) ||
+              Structures.eq_constr c (Lazy.force cTFArray) then
       match args with
         | ti :: te :: _ ->
            let ty = TFArray (of_coq reify known_logic ti,
@@ -221,8 +221,8 @@ let rec of_coq reify known_logic t =
       try Hashtbl.find reify.tbl t
       with Not_found ->
         let n = string_of_int (List.length reify.cuts) in
-        let compdec_name = Names.id_of_string ("CompDec"^n) in
-        let compdec_var = Term.mkVar compdec_name in
+        let compdec_name = Structures.mkId ("CompDec"^n) in
+        let compdec_var = Structures.mkVar compdec_name in
         let compdec_type = mklApp cCompDec [| t |]in
         reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
         let ce = mklApp cTyp_compdec [|t; compdec_var|] in
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 4f8d4ad..5d45ca4 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -13,11 +13,11 @@
 open SmtMisc
 
 
-type indexed_type = Term.constr gen_hashed
+type indexed_type = Structures.constr gen_hashed
 
 val dummy_indexed_type: int -> indexed_type
 val indexed_type_index : indexed_type -> int
-val indexed_type_hval : indexed_type -> Term.constr
+val indexed_type_hval : indexed_type -> Structures.constr
 
 type btype =
   | TZ
@@ -27,11 +27,11 @@ type btype =
   | TFArray of btype * btype
   | Tindex of indexed_type
 
-val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed
+val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed
 
 val equal : btype -> btype -> bool
 
-val to_coq : btype -> Term.constr
+val to_coq : btype -> Structures.constr
 
 val to_smt : Format.formatter -> btype -> unit
 
@@ -39,26 +39,26 @@ type reify_tbl
 
 val create : unit -> reify_tbl
 
-val declare : reify_tbl -> Term.constr -> Term.constr -> btype
+val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype
 
-val of_coq : reify_tbl -> logic -> Term.constr -> btype
+val of_coq : reify_tbl -> logic -> Structures.constr -> btype
 
-val get_coq_type_op : int -> Term.constr
+val get_coq_type_op : int -> Structures.constr
 
-val interp_tbl : reify_tbl -> Term.constr
+val interp_tbl : reify_tbl -> Structures.constr
 
 val to_list : reify_tbl ->  (int * indexed_type) list
 
-val make_t_i : reify_tbl -> Term.constr
+val make_t_i : reify_tbl -> Structures.constr
 
-val dec_interp : Term.constr -> btype -> Term.constr
-val ord_interp : Term.constr -> btype -> Term.constr
-val comp_interp : Term.constr -> btype -> Term.constr
-val inh_interp : Term.constr -> btype -> Term.constr
-val interp : Term.constr -> btype -> Term.constr
+val dec_interp : Structures.constr -> btype -> Structures.constr
+val ord_interp : Structures.constr -> btype -> Structures.constr
+val comp_interp : Structures.constr -> btype -> Structures.constr
+val inh_interp : Structures.constr -> btype -> Structures.constr
+val interp : Structures.constr -> btype -> Structures.constr
 
-val interp_to_coq : reify_tbl -> btype -> Term.constr
+val interp_to_coq : reify_tbl -> btype -> Structures.constr
 
-val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list
+val get_cuts : reify_tbl -> (Structures.id * Structures.types) list
 
 val logic : btype -> logic
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 1a990f1..78c07b9 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -10,10 +10,6 @@
 (**************************************************************************)
 
 
-open Entries
-open Declare
-open Decl_kinds
-
 open SmtMisc
 open CoqTerms
 open SmtForm
@@ -132,19 +128,19 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
 
   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 ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) 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 ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) 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 ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) 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 ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in
 
   (* EMPTY LEMMA LIST *)
   let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
@@ -167,14 +163,14 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
     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 roots in
-  let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
+  let _ = Structures.declare_constant root ce3 in
   let ce3' = Structures.mkUConst used_roots in
-  let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
+  let _ = Structures.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in
 
   ()
 
@@ -188,15 +184,15 @@ let interp_roots t_i roots =
     | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
 
 let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = mkName "t_i" in
-  let ntfunc = mkName "t_func" in
-  let ntatom = mkName "t_atom" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
-  let nused_roots = mkName "used_roots" in
-  let nd = mkName "d" in
+  let nti = Structures.mkName "t_i" in
+  let ntfunc = Structures.mkName "t_func" in
+  let ntatom = Structures.mkName "t_atom" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
+  let nused_roots = Structures.mkName "used_roots" in
+  let nd = Structures.mkName "d" in
 
-  let v = Term.mkRel in
+  let v = Structures.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -230,50 +226,50 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
   let theorem_proof_cast =
-    Term.mkCast (
-        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-        Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-        Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-        Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-        Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-        Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-        Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+    Structures.mkCast (
+        Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+        Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+        Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+        Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+        Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+        Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
         mklApp cchecker_correct
                [|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*);
 	         vm_cast_true_no_check
 	           (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*)|])|]))))))),
-        Term.VMcast,
+        Structures.vmcast,
         theorem_concl)
   in
   let theorem_proof_nocast =
-        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-        Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-        Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-        Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-        Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-        Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-        Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+        Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+        Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+        Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+        Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+        Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+        Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
         mklApp cchecker_correct
                [|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 ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in
-  let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
+  let _ = Structures.declare_constant name ce in
   ()
 
 
 (* Given an SMT-LIB2 file and a certif, call the checker *)
 
 let checker (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = mkName "t_i" in
-  let ntfunc = mkName "t_func" in
-  let ntatom = mkName "t_atom" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
-  let nused_roots = mkName "used_roots" in
-  let nd = mkName "d" in
+  let nti = Structures.mkName "t_i" in
+  let ntfunc = Structures.mkName "t_func" in
+  let ntatom = Structures.mkName "t_atom" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
+  let nused_roots = Structures.mkName "used_roots" in
+  let nd = Structures.mkName "d" in
 
-  let v = Term.mkRel in
+  let v = Structures.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -306,18 +302,18 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
     Structures.mkArray (Lazy.force cint, res) in
 
   let tm =
-   Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-   Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-   Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-   Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-   Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-   Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-   Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+   Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+   Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+   Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+   Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+   Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+   Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+   Structures.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 = 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
+    (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then
         "true" else "false")
 
 let count_used confl =
@@ -333,15 +329,15 @@ let count_used confl =
 
 
 let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = mkName "t_i" in
-  let ntfunc = mkName "t_func" in
-  let ntatom = mkName "t_atom" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
-  let nused_roots = mkName "used_roots" in
-  let nd = mkName "d" in
+  let nti = Structures.mkName "t_i" in
+  let ntfunc = Structures.mkName "t_func" in
+  let ntatom = Structures.mkName "t_atom" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
+  let nused_roots = Structures.mkName "used_roots" in
+  let nd = Structures.mkName "d" in
 
-  let v = Term.mkRel in
+  let v = Structures.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -376,16 +372,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
     Structures.mkArray (Lazy.force cint, res) in
 
   let tm =
-   Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-   Term.mkLetIn (ntfunc, t_func,
+   Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+   Structures.mkLetIn (ntfunc, t_func,
                  mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-   Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-   Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-   Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
+   Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+   Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+   Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
                                               v 2 (*t_atom*); v 1 (*t_form*)|],
-   Term.mkLetIn (nused_roots, used_rootsCstr,
+   Structures.mkLetIn (nused_roots, used_rootsCstr,
                  mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-   Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+   Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
    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
 
@@ -394,54 +390,54 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
          [|mklApp cprod
              [|Lazy.force cnat; Lazy.force cname_step|]|]) in
 
-  match Term.decompose_app res with
-  | c, _ when Term.eq_constr c (Lazy.force cNone) ->
+  match Structures.decompose_app res with
+  | c, _ when Structures.eq_constr c (Lazy.force cNone) ->
     Structures.error ("Debug checker is only meant to be used for certificates \
                        that fail to be checked by SMTCoq.")
-  | c, [_; n] when Term.eq_constr c (Lazy.force cSome) ->
-    (match Term.decompose_app n with
-     | c, [_; _; cnb; cn] when Term.eq_constr c (Lazy.force cpair) ->
-       let n = fst (Term.decompose_app cn) in
+  | c, [_; n] when Structures.eq_constr c (Lazy.force cSome) ->
+    (match Structures.decompose_app n with
+     | c, [_; _; cnb; cn] when Structures.eq_constr c (Lazy.force cpair) ->
+       let n = fst (Structures.decompose_app cn) in
        let name =
-         if Term.eq_constr n (Lazy.force cName_Res ) then "Res"
-         else if Term.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
-         else if Term.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
-         else if Term.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
-         else if Term.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
-         else if Term.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
-         else if Term.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
-         else if Term.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
-         else if Term.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
-         else if Term.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
-         else if Term.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
-         else if Term.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
-         else if Term.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
-         else if Term.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
-         else if Term.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
-         else if Term.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
-         else if Term.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
-         else if Term.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
-         else if Term.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
-         else if Term.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
-         else if Term.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
-         else if Term.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
-         else if Term.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
-         else if Term.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
-         else if Term.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
-         else if Term.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
-         else if Term.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
-         else if Term.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
-         else if Term.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
-         else if Term.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
-         else if Term.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
-         else if Term.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
-         else if Term.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
-         else if Term.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
-         else if Term.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
-         else if Term.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
-         else if Term.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
-         else if Term.eq_constr n (Lazy.force cName_Ext) then "Ext"
-         else if Term.eq_constr n (Lazy.force cName_Hole) then "Hole"
+         if Structures.eq_constr n (Lazy.force cName_Res ) then "Res"
+         else if Structures.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
+         else if Structures.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
+         else if Structures.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
+         else if Structures.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
+         else if Structures.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
+         else if Structures.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
+         else if Structures.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
+         else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
+         else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
+         else if Structures.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
+         else if Structures.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
+         else if Structures.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
+         else if Structures.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
+         else if Structures.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
+         else if Structures.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
+         else if Structures.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
+         else if Structures.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
+         else if Structures.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
+         else if Structures.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
+         else if Structures.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
+         else if Structures.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
+         else if Structures.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
+         else if Structures.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
+         else if Structures.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
+         else if Structures.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
+         else if Structures.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
+         else if Structures.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
+         else if Structures.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
+         else if Structures.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
+         else if Structures.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
+         else if Structures.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
+         else if Structures.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
+         else if Structures.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
+         else if Structures.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
+         else if Structures.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
+         else if Structures.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
+         else if Structures.eq_constr n (Lazy.force cName_Ext) then "Ext"
+         else if Structures.eq_constr n (Lazy.force cName_Hole) then "Hole"
          else string_coq_constr n
        in
        let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in
@@ -454,9 +450,9 @@ 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) ->
+ *   match Structures.decompose_app cl with
+ *   | c, _ when Structures.eq_constr c (Lazy.force cnil) -> []
+ *   | c, [_; x; cr] when Structures.eq_constr c (Lazy.force ccons) ->
  *     x :: of_coq_list cr
  *   | _ -> assert false *)
 
@@ -466,26 +462,22 @@ let checker_debug (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 ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) 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
+ *     Structures.mkConst (Structures.declare_constant t_func ce6) 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
+ *     Structures.mkConst (Structures.declare_constant t_atom ce1) 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
+ *     Structures.mkConst (Structures.declare_constant t_form ce2) in
  * 
  *   let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
  *       (interp_conseq_uf ct_i)
@@ -509,18 +501,15 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *     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 _ = Structures.declare_constant root ce3 in
  *   let ce3' = Structures.mkUConst cused_roots in
- *   let _ = declare_constant used_root
- *       (DefinitionEntry ce3', IsDefinition Definition) in
+ *   let _ = Structures.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in
  * 
  *   let setup =
  *    mklApp csetup_checker_step_debug
@@ -532,8 +521,8 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *            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) ->
+ *   let s, steps = match Structures.decompose_app setup with
+ *     | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) ->
  *       s, of_coq_list csteps
  *     | _ -> assert false
  *   in
@@ -550,12 +539,12 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *       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) ->
+ *     match Structures.decompose_app res with
+ *     | c, [_; _; s; cbad] when Structures.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)) ^ ")" ^
+ *                                (fst (Structures.decompose_app step)) ^ ")" ^
  *                              " of the certificate likely failed." )
  *     | _ -> assert false
  *   in
@@ -570,13 +559,13 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
 (* Tactic *)
 
 let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
-  let nti = mkName "t_i" in
-  let ntfunc = mkName "t_func" in
-  let ntatom = mkName "t_atom" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
+  let nti = Structures.mkName "t_i" in
+  let ntfunc = Structures.mkName "t_func" in
+  let ntatom = Structures.mkName "t_atom" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
 
-  let v = Term.mkRel in
+  let v = Structures.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
@@ -594,11 +583,11 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
         mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
   let add_lets t =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
-    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif
+    Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+    Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    Structures.mkLetIn (nc, certif, mklApp ccertif
              [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
     t))))) in
 
@@ -625,13 +614,13 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
 
 
 let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
-  let nti = mkName "t_i" in
-  let ntfunc = mkName "t_func" in
-  let ntatom = mkName "t_atom" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
+  let nti = Structures.mkName "t_i" in
+  let ntfunc = Structures.mkName "t_func" in
+  let ntatom = Structures.mkName "t_atom" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
 
-  let v = Term.mkRel in
+  let v = Structures.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
@@ -644,11 +633,11 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
   let add_lets t =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
-    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif
+    Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+    Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    Structures.mkLetIn (nc, certif, mklApp ccertif
              [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
     t))))) in
 
@@ -676,10 +665,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
 
 
 let get_arguments concl =
-  let f, args = Term.decompose_app concl in
+  let f, args = Structures.decompose_app concl in
   match args with
-  | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b
-  | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
+  | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b
+  | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
@@ -699,18 +688,18 @@ let of_coq_lemma rt ro ra' rf' env sigma solver_logic clemma =
   let env_lemma = List.fold_right Environ.push_rel rel_context env in
   let forall_args =
     let fmap r = let n, t = Structures.destruct_rel_decl r in
-                 string_of_name n, SmtBtype.of_coq rt solver_logic t in
+                 Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in
     List.map fmap rel_context in
-  let f, args = Term.decompose_app qf_lemma in
+  let f, args = Structures.decompose_app qf_lemma in
   let core_f =
-    if Term.eq_constr f (Lazy.force cis_true) then
+    if Structures.eq_constr f (Lazy.force cis_true) then
       match args with
       | [a] -> a
       | _ -> raise Axiom_form_unsupported
-    else if Term.eq_constr f (Lazy.force ceq) then
+    else if Structures.eq_constr f (Lazy.force ceq) then
       match args with
-      | [ty; arg1; arg2] when Term.eq_constr ty (Lazy.force cbool) &&
-                                Term.eq_constr arg2 (Lazy.force ctrue) ->
+      | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) &&
+                                Structures.eq_constr arg2 (Lazy.force ctrue) ->
          arg1
       | _ -> raise Axiom_form_unsupported
     else raise Axiom_form_unsupported in
@@ -730,7 +719,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
   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
 
-  let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
+  let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t =
     Hashtbl.create 100 in
   let new_ref ((l, pl), ls) =
     Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
@@ -752,10 +741,10 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
       | _ -> failwith "unexpected form of root" in
 
   let (body_cast, body_nocast, cuts) =
-    if ((Term.eq_constr b (Lazy.force ctrue)) ||
-        (Term.eq_constr b (Lazy.force cfalse))) then
+    if ((Structures.eq_constr b (Lazy.force ctrue)) ||
+        (Structures.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
-      let nl = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
       let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
       let lsmt = Form.flatten rf nl :: lsmt in
       let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
@@ -776,7 +765,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
 
   List.fold_right (fun (eqn, eqt) tac ->
       Structures.tclTHENLAST
-        (Structures.assert_before (Names.Name eqn) eqt)
+        (Structures.assert_before (Structures.name_of_id eqn) eqt)
         tac
     ) cuts
     (Structures.tclTHEN
@@ -804,7 +793,7 @@ let string_index_of_constr env i cf =
   try
     let s = string_coq_constr cf in
     let nc = Environ.named_context env in
-    let nd = Environ.lookup_named (Names.id_of_string s) env in
+    let nd = Environ.lookup_named (Structures.mkId s) env in
     let cpt = ref 0 in
     (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc
      with Exit -> ());
@@ -814,14 +803,13 @@ let string_index_of_constr env i cf =
 
 let vstring_i env i =
   let cf = SmtAtom.Atom.get_coq_term_op i in
-  if Term.isRel cf then
-    let dbi = Term.destRel cf in
+  if Structures.isRel cf then
+    let dbi = Structures.destRel cf in
     let s =
       Environ.lookup_rel dbi env
       |> Structures.get_rel_dec_name
-      |> function
-      | Names.Name id -> Names.string_of_id id
-      | Names.Anonymous -> "?" in
+      |> SmtMisc.string_of_name_def "?"
+    in
     s, dbi
   else
     string_index_of_constr env i cf
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index d7b6ae6..9a1b681 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -11,13 +11,13 @@
 
 
 val parse_certif :
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
   SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
   SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
@@ -29,7 +29,7 @@ val checker_debug :
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a
 
 val theorem :
-  Structures.names_id ->
+  Structures.id ->
   SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
   SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
@@ -56,8 +56,8 @@ val tactic :
   SmtAtom.Form.reify ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
-  (Environ.env -> Term.constr -> Term.constr) ->
-  Term.constr list ->
+  (Environ.env -> Structures.constr -> Structures.constr) ->
+  Structures.constr list ->
   Structures.constr_expr list -> Structures.tactic
 
 val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index ad6a5a4..20b99ac 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -82,7 +82,7 @@ module type FORM =
     val get : ?declare:bool -> reify -> pform -> t
 
     (** Give a coq term, build the corresponding formula *)
-    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
 
     val hash_hform : (hatom -> hatom) -> reify -> t -> t
     (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
@@ -94,20 +94,20 @@ module type FORM =
 
     (** Producing Coq terms *)
 
-    val to_coq : t -> Term.constr
+    val to_coq : t -> Structures.constr
 
     val pform_tbl : reify -> pform array
 
     val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-    val interp_tbl : reify -> Term.constr * Term.constr
+    val interp_tbl : reify -> Structures.constr * Structures.constr
     val nvars : reify -> int
     (** Producing a Coq term corresponding to the interpretation
           of a formula *)
     (** [interp_atom] map [hatom] to coq term, it is better if it produce
           shared terms. *)
     val interp_to_coq :
-      (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
-      t -> Term.constr
+      (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
+      t -> Structures.constr
   end
 
 module Make (Atom:ATOM) =
@@ -361,9 +361,9 @@ module Make (Atom:ATOM) =
       | CCunknown
 
     module ConstrHash = struct
-      type t = Term.constr
-      let equal = Term.eq_constr
-      let hash = Term.hash_constr
+      type t = Structures.constr
+      let equal = Structures.eq_constr
+      let hash = Structures.hash_constr
     end
     module ConstrHashtbl = Hashtbl.Make(ConstrHash)
 
@@ -386,7 +386,7 @@ module Make (Atom:ATOM) =
       let get_cst c =
         try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
       let rec mk_hform h =
-        let c, args = Term.decompose_app h in
+        let c, args = Structures.decompose_app h in
         match get_cst c with
           | CCtrue  -> get reify (Fapp(Ftrue,empty_args))
           | CCfalse -> get reify (Fapp(Ffalse,empty_args))
@@ -427,8 +427,8 @@ module Make (Atom:ATOM) =
       and mk_fnot i args =
         match args with
           | [t] ->
-             let c,args = Term.decompose_app t in
-             if Term.eq_constr c (Lazy.force cnegb) then
+             let c,args = Structures.decompose_app t in
+             if Structures.eq_constr c (Lazy.force cnegb) then
                mk_fnot (i+1) args
              else
                let q,r = i lsr 1 , i land 1 in
@@ -442,8 +442,8 @@ module Make (Atom:ATOM) =
         match args with
           | [t1;t2] ->
              let l2 = mk_hform t2 in
-             let c, args = Term.decompose_app t1 in
-             if Term.eq_constr c (Lazy.force candb) then
+             let c, args = Structures.decompose_app t1 in
+             if Structures.eq_constr c (Lazy.force candb) then
                mk_fand (l2::acc) args
              else
                let l1 = mk_hform t1 in
@@ -454,8 +454,8 @@ module Make (Atom:ATOM) =
         match args with
           | [t1;t2] ->
              let l2 = mk_hform t2 in
-             let c, args = Term.decompose_app t1 in
-             if Term.eq_constr c (Lazy.force corb) then
+             let c, args = Structures.decompose_app t1 in
+             if Structures.eq_constr c (Lazy.force corb) then
                mk_for (l2::acc) args
              else
                let l1 = mk_hform t1 in
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index c26e279..ba8c066 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -12,10 +12,10 @@
 
 open SmtMisc
 
-module type ATOM = 
-  sig 
+module type ATOM =
+  sig
 
-    type t 
+    type t
     val index : t -> int
 
     val equal : t -> t -> bool
@@ -25,7 +25,7 @@ module type ATOM =
     val to_smt : Format.formatter -> t -> unit
     val logic : t -> logic
 
-  end 
+  end
 
 
 type fop =
@@ -38,16 +38,16 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
-  | Fforall of (string * SmtBtype.btype) list 
- 
-type ('a,'f) gen_pform = 
+  | Fforall of (string * SmtBtype.btype) list
+
+type ('a,'f) gen_pform =
   | Fatom of 'a
   | Fapp of fop * 'f array
   | FbbT of 'a * 'f list
 
 module type FORM =
-  sig 
-    type hatom 
+  sig
+    type hatom
     type t
     type pform = (hatom, t) gen_pform
 
@@ -72,16 +72,16 @@ module type FORM =
 
       (* Building formula from positive formula *)
       exception NotWellTyped of pform
-      type reify 
+      type reify
       val create : unit -> reify
       val clear : reify -> unit
       val get : ?declare:bool -> reify -> pform -> t
-      
-      (** Given a coq term, build the corresponding formula *)  
-      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+
+      (** Given a coq term, build the corresponding formula *)
+      val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
 
       val hash_hform : (hatom -> hatom) -> reify -> t -> t
-                                             
+
       (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
       val flatten : reify -> t -> t
 
@@ -89,24 +89,22 @@ module type FORM =
           counter-parts *)
       val right_assoc : reify -> t -> t
 
-      (** Producing Coq terms *) 
+      (** Producing Coq terms *)
 
-      val to_coq : t -> Term.constr
+      val to_coq : t -> Structures.constr
 
       val pform_tbl : reify -> pform array
 
       val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-      val interp_tbl : reify -> Term.constr * Term.constr
-      val nvars : reify -> int 
-      (** Producing a Coq term corresponding to the interpretation 
+      val interp_tbl : reify -> Structures.constr * Structures.constr
+      val nvars : reify -> int
+      (** Producing a Coq term corresponding to the interpretation
           of a formula *)
       (** [interp_atom] map [hatom] to coq term, it is better if it produce
           shared terms. *)
-      val interp_to_coq : 
-	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
-	    t -> Term.constr
+      val interp_to_coq :
+	  (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
+	    t -> Structures.constr
   end
 
 module Make (Atom:ATOM) : FORM with type hatom = Atom.t
-
-	
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index f839869..92f0f09 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -25,16 +25,9 @@ type 'a gen_hashed = { index : int; hval : 'a }
 
 (** Functions over constr *)
 
-let mklApp f args = Term.mkApp (Lazy.force f, args)
-
-(* TODO : Set -> Type *)
-let declare_new_type = Structures.declare_new_type
-let declare_new_variable = Structures.declare_new_variable
-
-let mkName s =
-  let id = Names.id_of_string s in
-  Names.Name id
+let mklApp f args = Structures.mkApp (Lazy.force f, args)
 
+let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
 
 let string_coq_constr t =
   let rec fix rf x = rf (fix rf) x in
@@ -43,11 +36,6 @@ let string_coq_constr t =
   Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t))
 
 
-let string_of_name = function
-    Names.Name id -> Names.string_of_id id
-  | _ -> failwith "unnamed rel"
-
-
 (** Logics *)
 
 type logic_item =
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index a9de935..f3bcf60 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -10,15 +10,12 @@
 (**************************************************************************)
 
 
-val cInt_tbl : (int, Term.constr) Hashtbl.t
-val mkInt : int -> Term.constr
+val cInt_tbl : (int, Structures.constr) Hashtbl.t
+val mkInt : int -> Structures.constr
 type 'a gen_hashed = { index : int; hval : 'a; }
-val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.types -> Term.constr
-val mkName : string -> Names.name
-val string_coq_constr : Term.constr -> string
-val string_of_name : Names.name -> string
+val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr
+val string_of_name_def : string -> Structures.name -> string
+val string_coq_constr : Structures.constr -> string
 type logic_item = LUF | LLia | LBitvectors | LArrays
 module SL : Set.S with type elt = logic_item
 type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index a9855a2..5d9d82d 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -458,10 +458,10 @@ let to_coq to_lit interp (cstep,
         | Ext (res) -> mklApp cExt [|out_c c; out_f res|]
         | Hole (prem_id, concl) ->
            let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in
-           let ass_name = Names.id_of_string ("ass"^(string_of_int (Hashtbl.hash concl))) in
+           let ass_name = Structures.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in
            let ass_ty = interp (prem, concl) in
            cuts := (ass_name, ass_ty)::!cuts;
-           let ass_var = Term.mkVar ass_name in
+           let ass_var = Structures.mkVar ass_name in
            let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in
            let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in
            let concl' = out_cl concl in
@@ -471,8 +471,8 @@ let to_coq to_lit interp (cstep,
              | Some find -> find cl
              | None -> assert false in
            let concl' = out_cl [concl] in
-           let app_name = Names.id_of_string ("app" ^ (string_of_int (Hashtbl.hash concl))) in
-           let app_var = Term.mkVar app_name in
+           let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
+           let app_var = Structures.mkVar app_name in
            let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
            cuts := (app_name, app_ty)::!cuts;
            mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index f06ade4..5ded32a 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -47,26 +47,26 @@ val alloc : 'a SmtCertif.clause -> int
 val naive_alloc : 'a SmtCertif.clause -> int
 val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
 val to_coq :
-  ('a -> Term.constr) ->
-  ('a list list * 'a list -> Term.types) ->
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t * Term.constr Lazy.t ->
+  ('a -> Structures.constr) ->
+  ('a list list * 'a list -> Structures.types) ->
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
+  Structures.constr Lazy.t * Structures.constr Lazy.t ->
   'a SmtCertif.clause ->
-  ('a SmtCertif.clause -> Term.types * Term.constr) option ->
-  Term.constr * 'a SmtCertif.clause *
-    (Names.identifier * Term.types) list
+  ('a SmtCertif.clause -> Structures.types * Structures.constr) option ->
+  Structures.constr * 'a SmtCertif.clause *
+    (Structures.id * Structures.types) list
 module MakeOpt :
   functor (Form : SmtForm.FORM) ->
     sig
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 468aa1e..6fa62d8 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -11,13 +11,13 @@
 
 
 val parse_certif :
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id ->
-  Structures.names_id -> Structures.names_id -> Structures.names_id -> string -> string -> unit
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id ->
+  Structures.id -> Structures.id -> Structures.id -> string -> string -> unit
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
-val theorem : Structures.names_id -> string -> string -> unit
-val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Term.constr list -> Structures.constr_expr list -> Structures.tactic
+val theorem : Structures.id -> string -> string -> unit
+val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index dbf3d62..13beb9d 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -14,9 +14,80 @@ open Entries
 open Coqlib
 
 
+(* Constr generation and manipulation *)
+type id = Names.id
+let mkId = Names.id_of_string
+
+
+type name = Names.name
+let name_of_id i = Names.Name i
+let mkName s =
+  let id = mkId s in
+  name_of_id id
+let string_of_name = function
+    Names.Name id -> Names.string_of_id id
+  | _ -> failwith "unnamed rel"
+
+
+type constr = Term.constr
+type types = Term.types
+let eq_constr = Term.eq_constr
+let hash_constr = Term.hash_constr
+let mkProp = Term.mkProp
+let mkConst = Constr.mkConst
+let mkVar = Term.mkVar
+let mkRel = Term.mkRel
+let isRel = Term.isRel
+let destRel = Term.destRel
+let lift = Term.lift
+let mkApp = Term.mkApp
+let decompose_app = Term.decompose_app
+let mkLambda = Term.mkLambda
+let mkProd = Term.mkProd
+let mkLetIn = Term.mkLetIn
+
+let pr_constr_env = Printer.pr_constr_env
+let pr_constr = Printer.pr_constr
+
+let mkUConst c =
+  { const_entry_body = c;
+    const_entry_type = None;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+let mkTConst c _ ty =
+  { const_entry_body = c;
+    const_entry_type = Some ty;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+(* TODO : Set -> Type *)
+let declare_new_type t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force Term.mkSet) [] false None (dummy_loc, t);
+  Term.mkVar t
+
+let declare_new_variable v constr_t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
+  Term.mkVar v
+
+let declare_constant n c =
+  Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
 
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
+type cast_kind = Term.cast_kind
+let vmcast = Term.VMcast
+let mkCast = Term.mkCast
+
+
+(* EConstr *)
+type econstr = Term.constr
+let econstr_of_constr e = e
+
+
+(* Modules *)
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 
 (* Int63 *)
@@ -64,58 +135,24 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
   mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace)
 
 
-(* Differences between the two versions of Coq *)
-type names_id_t = Names.identifier
-
-let dummy_loc = Pp.dummy_loc
-
-let mkUConst c =
-  { const_entry_body = c;
-    const_entry_type = None;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-let mkTConst c _ ty =
-  { const_entry_body = c;
-    const_entry_type = Some ty;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-let error = Errors.error
-
-let coqtype = lazy Term.mkSet
-
-let declare_new_type t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (dummy_loc, t);
-  Term.mkVar t
-
-let declare_new_variable v constr_t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
-  Term.mkVar v
-
-let extern_constr = Constrextern.extern_constr true Environ.empty_env
-
-let vernacentries_interp expr =
-  Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr))
-
-let pr_constr_env = Printer.pr_constr_env
+(* Micromega *)
+module Micromega_plugin_Certificate = Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega
+module Micromega_plugin_Micromega = Micromega
+module Micromega_plugin_Mutils = Mutils
 
-let lift = Term.lift
+let micromega_coq_proofTerm =
+  Coq_micromega.M.coq_proofTerm
 
-let destruct_rel_decl (n, _, t) = n, t
+let micromega_dump_proof_term p =
+  Coq_micromega.dump_proof_term p
 
-let interp_constr env sigma = Constrintern.interp_constr sigma env
 
+(* Tactics *)
 let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 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
@@ -123,6 +160,12 @@ let mk_tactic tac gl =
   tac env sigma t gl
 let set_evars_tac _ = Tacticals.tclIDTAC
 
+
+(* Other differences between the two versions of Coq *)
+let error = Errors.error
+let extern_constr = Constrextern.extern_constr true Environ.empty_env
+let destruct_rel_decl (n, _, t) = n, t
+let interp_constr env sigma = Constrintern.interp_constr sigma env
 let ppconstr_lsimpleconstr = Ppconstr.lsimple
 let constrextern_extern_constr =
   let env = Global.env () in
@@ -133,25 +176,7 @@ 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
 
+let vm_conv = Reduction.vm_conv
+let cbv_vm = Vnorm.cbv_vm
 
-(* 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 9ec21d2..abedc17 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -10,49 +10,74 @@
 (**************************************************************************)
 
 
-val gen_constant : string list list -> string -> Term.constr lazy_t
+(* Constr generation and manipulation *)
+type id
+val mkId : string -> id
+
+type name
+val name_of_id : id -> name
+val mkName : string -> name
+val string_of_name : name -> string
+
+type constr = Term.constr
+type types = constr
+val eq_constr : constr -> constr -> bool
+val hash_constr : constr -> int
+val mkProp : types
+val mkConst : Names.Constant.t -> constr
+val mkVar : id -> constr
+val mkRel : int -> constr
+val isRel : constr -> bool
+val destRel : constr -> int
+val lift : int -> constr -> constr
+val mkApp : constr -> constr array -> constr
+val decompose_app : constr -> constr * constr list
+val mkLambda : name * types * constr -> constr
+val mkProd : name * types * types -> types
+val mkLetIn : name * constr * types * constr -> constr
+
+val pr_constr_env : Environ.env -> constr -> Pp.t
+val pr_constr : constr -> Pp.t
+
+val mkUConst : constr -> Entries.definition_entry
+val mkTConst : constr -> 'a -> types -> Entries.definition_entry
+val declare_new_type : id -> types
+val declare_new_variable : id -> types -> constr
+val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+
+type cast_kind
+val vmcast : cast_kind
+val mkCast : constr * cast_kind * constr -> constr
+
+
+(* EConstr *)
+type econstr = constr
+val econstr_of_constr : constr -> econstr
+
+
+(* Modules *)
+val gen_constant : string list list -> string -> constr lazy_t
+
+
+(* Int63 *)
 val int63_modules : string list list
-val mkInt : int -> Term.constr
-val cint : Term.constr lazy_t
+val mkInt : int -> constr
+val cint : constr lazy_t
+
+
+(* PArray *)
 val parray_modules : string list list
 val max_array_size : int
-val mkArray : Term.types * Term.constr array -> Term.constr
+val mkArray : types * constr array -> constr
+
+
+(* Traces *)
 val mkTrace :
-  ('a -> Term.constr) ->
+  ('a -> constr) ->
   ('a -> 'a) ->
-  Term.constr Lazy.t ->
+  constr Lazy.t ->
   'b ->
-  'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr
-type names_id_t = Names.identifier
-val mkUConst : Term.constr -> Entries.definition_entry
-val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry
-val error : string -> 'a
-val coqtype : Term.types lazy_t
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.types -> Term.constr
-val extern_constr : Term.constr -> Topconstr.constr_expr
-val vernacentries_interp : Topconstr.constr_expr -> unit
-val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
-val lift : int -> Term.constr -> Term.constr
-val destruct_rel_decl : Term.rel_declaration -> Names.name * Term.constr
-val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term.constr
-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) ->
-  Proof_type.goal Tacmach.sigma -> 'a
-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
+  'c -> 'd -> 'e -> int -> types -> constr -> 'a ref -> constr
 
 
 (* Micromega *)
@@ -61,15 +86,33 @@ 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
+val micromega_coq_proofTerm : constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
 
 
-(* Types in the Coq source code *)
+(* Tactics *)
 type tactic = Proof_type.tactic
-type names_id = Names.identifier
+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 : name -> types -> Proof_type.tactic
+val vm_cast_no_check : constr -> Proof_type.tactic
+val mk_tactic :
+  (Environ.env ->
+   Evd.evar_map -> types -> Proof_type.goal Tacmach.sigma -> 'a) ->
+  Proof_type.goal Tacmach.sigma -> 'a
+val set_evars_tac : 'a -> Proof_type.tactic
+
+
+(* Other differences between the two versions of Coq *)
 type constr_expr = Topconstr.constr_expr
+val error : string -> 'a
+val extern_constr : constr -> Topconstr.constr_expr
+val destruct_rel_decl : Term.rel_declaration -> name * constr
+val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr
+val ppconstr_lsimpleconstr : Ppconstr.precedence
+val constrextern_extern_constr : constr -> Topconstr.constr_expr
+val get_rel_dec_name : 'a -> name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
 
-(* EConstr *)
-type econstr = Term.constr
-val econstr_of_constr : Term.constr -> econstr
+val vm_conv : Reduction.conv_pb -> types Reduction.conversion_function
+val cbv_vm : Environ.env -> constr -> types -> constr
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index 9a90d39..9a79f04 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -300,7 +300,7 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
 
 Axiom diveucl_21_spec :  forall a1 a2 b,
    let (q,r) := diveucl_21 a1 a2 b in
-   ([|q|],[|r|]) = Zdiv_eucl ([|a1|] * wB + [|a2|]) [|b|].
+   ([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|].
 
 Axiom addmuldiv_def_spec : forall p x y,
   addmuldiv p x y = addmuldiv_def p x y.
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index 9f24c54..726bffd 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -131,7 +131,7 @@ Admitted.
 (** translation with Z *)
 Require Import Ndigits.
 
-Lemma Z_of_N_double : forall n, Z_of_N (Ndouble n) = Zdouble (Z_of_N n).
+Lemma Z_of_N_double : forall n, Z_of_N (N.double n) = Z.double (Z_of_N n).
 Proof.
  destruct n;simpl;trivial.
 Qed.
@@ -148,7 +148,7 @@ Proof. apply phi_bounded. Qed.
 (*  rewrite inj_S;simpl;assert (W:= IHn (x >> 1)%int). *)
 (*  rewrite Zpower_Zsucc;auto with zarith. *)
 (*  destruct (is_even x). *)
-(*  rewrite Zdouble_mult;auto with zarith. *)
+(*  rewrite Z.double_mult;auto with zarith. *)
 (*  rewrite Zdouble_plus_one_mult;auto with zarith. *)
 (* Qed. *)
 
@@ -183,7 +183,7 @@ Proof.
  red in Heq;rewrite Heq;trivial.
  rewrite <- not_true_iff_false, ltb_spec in Heq.
  case_eq (x == y)%int;intros Heq1.
- rewrite eqb_spec in Heq1;rewrite Heq1, Zcompare_refl;trivial.
+ rewrite eqb_spec in Heq1;rewrite Heq1, Z.compare_refl;trivial.
  rewrite <- not_true_iff_false, eqb_spec in Heq1.
  symmetry;change ([|x|] > [|y|]);rewrite <- to_Z_eq in Heq1;omega.
 Qed.
@@ -331,11 +331,11 @@ Proof. intros; unfold pred; apply sub_spec. Qed.
 Lemma diveucl_spec :
   forall x y,
     let (q,r) := diveucl x y in
-    ([|q|],[|r|]) = Zdiv_eucl [|x|] [|y|].
+    ([|q|],[|r|]) = Z.div_eucl [|x|] [|y|].
 Proof.
  intros;rewrite diveucl_def_spec.
  unfold diveucl_def;rewrite div_spec, mod_spec.
- unfold Zdiv, Zmod;destruct (Zdiv_eucl [|x|] [|y|]);trivial.
+ unfold Z.div, Zmod;destruct (Z.div_eucl [|x|] [|y|]);trivial.
 Qed.
 
 (* Sqrt *)
@@ -358,26 +358,26 @@ Proof.
  apply  Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith.
  intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk.
  rewrite Zmult_0_r, Zplus_0_r, Zplus_0_l.
- generalize (sqr_pos (Zsucc j / 2)) (quotient_by_2 (Zsucc j));
-   unfold Zsucc.
+ generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j));
+   unfold Z.succ.
  rewrite Zpower_2, Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r.
  auto with zarith.
  intros k Hk _.
- replace ((Zsucc j + Zsucc k) / 2) with ((j + k)/2 + 1).
+ replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1).
  generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)).
- unfold Zsucc; repeat rewrite Zpower_2;
+ unfold Z.succ; repeat rewrite Zpower_2;
    repeat rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r.
  repeat rewrite Zmult_1_l; repeat rewrite Zmult_1_r.
  auto with zarith.
  rewrite Zplus_comm, <- Z_div_plus_full_l; auto with zarith.
- apply f_equal2 with (f := Zdiv); auto with zarith.
+ apply f_equal2 with (f := Z.div); auto with zarith.
 Qed.
 
 Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2.
 Proof.
  intros Hi Hj.
  assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith).
- apply Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij).
+ apply Z.lt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij).
  pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith.
 Qed.
 
@@ -402,7 +402,7 @@ Qed.
 Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i.
 Proof.
  intros Hi Hj Hd; rewrite Zpower_2.
- apply Zle_trans with (j * (i/j)); auto with zarith.
+ apply Z.le_trans with (j * (i/j)); auto with zarith.
  apply Z_mult_div_ge; auto with zarith.
 Qed.
 
@@ -411,7 +411,7 @@ Proof.
  intros Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto.
  intros H1; contradict H; apply Zle_not_lt.
  assert (2 * j <= j + (i/j)); auto with zarith.
- apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith.
+ apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith.
  apply Z_mult_div_ge; auto with zarith.
 Qed.
 
@@ -488,7 +488,7 @@ Proof.
  intros j3 Hj3 Hpj3.
  apply HHrec; auto.
  rewrite inj_S, Zpower_Zsucc.
- apply Zle_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith.
+ apply Z.le_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith.
  apply Zle_0_nat.
 Qed.
 
@@ -496,7 +496,7 @@ Lemma sqrt_spec : forall x,
        [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.
 Proof.
  intros i; unfold sqrt.
- rewrite compare_spec. case Zcompare_spec; rewrite to_Z_1;
+ rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1;
    intros Hi; auto with zarith.
  repeat rewrite Zpower_2; auto with zarith.
  apply iter_sqrt_correct; auto with zarith;
@@ -508,9 +508,9 @@ Proof.
   assert (W:= Z_mult_div_ge [|i|] 2);assert (W':= to_Z_bounded i);auto with zarith.
   intros j2 H1 H2; contradict H2; apply Zlt_not_le.
   fold wB;assert (W:=to_Z_bounded i).
-  apply Zle_lt_trans with ([|i|]); auto with zarith.
+  apply Z.le_lt_trans with ([|i|]); auto with zarith.
   assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith).
-  apply Zle_trans with (2 * ([|i|]/2)); auto with zarith.
+  apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith.
   apply Z_mult_div_ge; auto with zarith.
  case (to_Z_bounded i); repeat rewrite Zpower_2; auto with zarith.
 Qed.
@@ -543,8 +543,8 @@ Proof.
  assert (([|ih|] < [|j|] + 1)%Z); auto with zarith.
  apply Zlt_square_simpl; auto with zarith.
  simpl zn2z_to_Z in H1.
- repeat rewrite <-Zpower_2; apply Zle_lt_trans with (2 := H1).
- apply Zle_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith.
+ repeat rewrite <-Zpower_2; apply Z.le_lt_trans with (2 := H1).
+ apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith.
 Qed.
 
 
@@ -553,7 +553,7 @@ Lemma div2_phi ih il j:
 Proof.
  generalize (diveucl_21_spec ih il j).
  case diveucl_21; intros q r Heq.
- simpl zn2z_to_Z;unfold Zdiv;rewrite <- Heq;trivial.
+ simpl zn2z_to_Z;unfold Z.div;rewrite <- Heq;trivial.
 Qed.
 
 Lemma zn2z_to_Z_pos ih il : 0 <= [||WW ih il||].
@@ -577,9 +577,9 @@ Proof.
  case (to_Z_bounded il); intros Hil1 _.
  case (to_Z_bounded j); intros _ Hj1.
  assert (Hp3: (0 < [||WW ih il||])).
-  simpl zn2z_to_Z;apply Zlt_le_trans with ([|ih|] * wB)%Z; auto with zarith.
+  simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith.
   apply Zmult_lt_0_compat; auto with zarith.
-  apply Zlt_le_trans with (2:= Hih); auto with zarith.
+  apply Z.lt_le_trans with (2:= Hih); auto with zarith.
  cbv zeta.
  case_eq (ih < j)%int;intros Heq.
  rewrite ltb_spec in Heq.
@@ -642,11 +642,11 @@ Proof.
  apply sqrt_main; auto with zarith.
  contradict Hij; apply Zle_not_lt.
  assert ((1 + [|j|]) <= 2 ^ (Z_of_nat size - 1)); auto with zarith.
- apply Zle_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith.
+ apply Z.le_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith.
  assert (0 <= 1 + [|j|]); auto with zarith.
  apply Zmult_le_compat; auto with zarith.
  change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB).
- apply Zle_trans with ([|ih|] * wB); auto with zarith.
+ apply Z.le_trans with ([|ih|] * wB); auto with zarith.
  unfold zn2z_to_Z, wB; auto with zarith.
 Qed.
 
@@ -671,7 +671,7 @@ Proof.
  intros j3 Hj3 Hpj3.
  apply HHrec; auto.
  rewrite inj_S, Zpower_Zsucc.
- apply Zle_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith.
+ apply Z.le_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith.
  apply Zle_0_nat.
 Qed.
 
@@ -688,7 +688,7 @@ Lemma sqrt2_spec : forall x y,
   (intros s; ring).
  assert (Hb: 0 <= wB) by (red; intros HH; discriminate).
  assert (Hi2: [||WW ih il ||] < ([|max_int|] + 1) ^ 2).
-  apply Zle_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith.
+  apply Z.le_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith.
   2: apply refl_equal.
   case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4.
   unfold zn2z_to_Z; auto with zarith.
@@ -719,7 +719,7 @@ Lemma sqrt2_spec : forall x y,
  assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith.
  case (to_Z_bounded s); intros _ Hps.
  case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith.
- apply Zle_trans with (([|ih1|] + 2) * wB); auto with zarith.
+ apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith.
  rewrite Zmult_plus_distr_l.
  assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
  unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
@@ -734,7 +734,7 @@ Lemma sqrt2_spec : forall x y,
  apply Zlt_not_le; rewrite Zpower_2, Hihl1.
  unfold zn2z_to_Z.
  case (to_Z_bounded il); intros _ H2.
- apply Zlt_le_trans with (([|ih|] + 1) * wB + 0).
+ apply Z.lt_le_trans with (([|ih|] + 1) * wB + 0).
  rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith.
  case (to_Z_bounded il1); intros H3 _.
  apply Zplus_le_compat; auto with zarith.
@@ -750,7 +750,7 @@ Lemma sqrt2_spec : forall x y,
   rewrite sub_spec, Zmod_small; auto; replace [|1|] with 1; auto.
   case (to_Z_bounded ih); intros H1 H2.
   split; auto with zarith.
-  apply Zle_trans with (wB/4 - 1); auto with zarith.
+  apply Z.le_trans with (wB/4 - 1); auto with zarith.
  case_eq (ih1 < ih - 1)%int;  [idtac | rewrite <- not_true_iff_false];
   rewrite ltb_spec, Hsih; intros Heq.
  rewrite Zpower_2, Hihl1.
@@ -762,10 +762,10 @@ Lemma sqrt2_spec : forall x y,
   auto with zarith.
  rewrite <-Hil2.
  case (to_Z_bounded il2); intros Hpil2 _.
- apply Zle_trans with ([|ih|] * wB + - wB); auto with zarith.
+ apply Z.le_trans with ([|ih|] * wB + - wB); auto with zarith.
  case (to_Z_bounded s);  intros _ Hps.
  assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
- apply Zle_trans with ([|ih1|] * wB + 2 * wB); auto with zarith.
+ apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith.
  assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith.
  rewrite Zmult_plus_distr_l in Hi; auto with zarith.
  unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
@@ -786,10 +786,10 @@ Lemma sqrt2_spec : forall x y,
    contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1.
   unfold zn2z_to_Z.
   case (to_Z_bounded il); intros _ Hpil1.
-  apply Zlt_le_trans with (([|ih|] + 1) * wB).
+  apply Z.lt_le_trans with (([|ih|] + 1) * wB).
   rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith.
   case (to_Z_bounded il1); intros Hpil2 _.
-  apply Zle_trans with (([|ih1|]) * wB); auto with zarith.
+  apply Z.le_trans with (([|ih1|]) * wB); auto with zarith.
  contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1.
  unfold zn2z_to_Z; rewrite He.
  assert ([|il|] - [|il1|] < 0); auto with zarith.
@@ -880,7 +880,7 @@ Proof.
  unfold wB; change (Z_of_nat size) with [|digits|].
  replace ([|i|]) with (([|i|] - [|digits|]) + [|digits|])%Z; try ring.
  rewrite Zpower_exp, Zmult_assoc, Z_mod_mult; auto with arith.
- apply Zle_ge; auto with zarith.
+ apply Z.le_ge; auto with zarith.
  case (to_Z_bounded digits); auto with zarith.
 Qed.
 
@@ -905,7 +905,7 @@ Proof.
  case (to_Z_bounded digits); intros H1d H2d.
  rewrite leb_spec in H.
  apply Zdiv_small; split; auto.
- apply Zlt_le_trans with (1 := H2x).
+ apply Z.lt_le_trans with (1 := H2x).
  unfold wB; change (Z_of_nat size) with [|digits|].
  apply Zpower_le_monotone; auto with zarith.
 Qed.
@@ -940,8 +940,8 @@ Proof.
    rewrite add_spec, Zmod_small; auto with zarith.
  apply to_Z_inj; rewrite !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith.
  apply Zdiv_small; split; auto with zarith.
- apply Zlt_le_trans with (1 := H2i).
- apply Zle_trans with (1 := H).
+ apply Z.lt_le_trans with (1 := H2i).
+ apply Z.le_trans with (1 := H).
  apply Zpower2_le_lin; auto with zarith.
 Qed.
 
@@ -1082,10 +1082,10 @@ Admitted. (* Too slow *)
 (*    replace (2^[|1|]) with 2%Z;  auto with zarith. *)
 (*  apply Zdiv_lt_upper_bound; auto with zarith. *)
 (*  generalize H2i1; rewrite inj_S. *)
-(*  unfold Zsucc; rewrite Zpower_exp; auto with zarith. *)
+(*  unfold Z.succ; rewrite Zpower_exp; auto with zarith. *)
 (*  apply Zdiv_lt_upper_bound; auto with zarith. *)
 (*  generalize H2i2; rewrite inj_S. *)
-(*  unfold Zsucc; rewrite Zpower_exp; auto with zarith. *)
+(*  unfold Z.succ; rewrite Zpower_exp; auto with zarith. *)
 (*  intros i. *)
 (*  case (Zle_or_lt [|digits|] [|i|]); intros Hi. *)
 (*  rewrite !bit_M; auto; rewrite leb_spec; auto. *)
@@ -1157,17 +1157,14 @@ Proof.
  rewrite Zpower_exp; 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.
+ 2: apply Z.lt_gt; apply Zpower_gt_0; unfold d1; lia.
  pattern d1 at 2;
    replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z.
  2: unfold d1, d2; ring.
  rewrite Zpower_exp; auto with zarith.
- 2: unfold d2; auto with zarith.
  rewrite <-Zmult_assoc, Zmult_comm.
  rewrite Z_div_plus_l; auto with zarith.
- 2: unfold d2; auto with zarith.
  rewrite Zpower_exp, Zpower_1_r; auto with zarith.
  rewrite <-Zplus_mod_idemp_l.
  rewrite <-!Zmult_assoc, Zmult_comm, Z_mod_mult, Zplus_0_l; auto.
@@ -1452,11 +1449,11 @@ Proof.
  apply Zle_antisym.
  apply Zdiv_le_lower_bound; auto with zarith.
  assert (F2: [|x|] + [|z|] < 2 * wB); auto with zarith.
- generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith.
+ generalize (Zdiv_lt_upper_bound _ _ _ (Z.gt_lt _ _ F1) F2); auto with zarith.
  apply Zle_antisym.
  apply Zdiv_le_lower_bound; auto with zarith.
  assert (F2: [|x|] + [|y|] < 2 * wB); auto with zarith.
- generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith.
+ generalize (Zdiv_lt_upper_bound _ _ _ (Z.gt_lt _ _ F1) F2); auto with zarith.
 Qed.
 
 Lemma add_cancel_r x y z : (y + x = z + x)%int -> y = z.
@@ -1499,7 +1496,7 @@ Proof.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  intros n IH x y; rewrite inj_S.
- unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ unfold Z.succ; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
  intros Hx Hy.
  rewrite leb_spec.
  rewrite (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)).
@@ -1536,7 +1533,7 @@ Proof.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  intros n IH x y; rewrite inj_S.
- unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ unfold Z.succ; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
  intros Hx Hy.
  split.
  intros Hn.
@@ -1634,7 +1631,7 @@ Proof.
  split.
  case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith.
  rewrite add_spec.
- apply Zle_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith.
+ apply Z.le_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith.
  case (Zmod_le_first ([|x >> 1|] + [|y >> 1|]) wB); auto with zarith.
  case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith.
  generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1.
@@ -1798,22 +1795,22 @@ Qed.
 
 Lemma leb_trans : forall x y z, x <= y = true ->  y <= z = true -> x <= z = true.
 Proof.
- intros x y z;rewrite !leb_spec;apply Zle_trans.
+ intros x y z;rewrite !leb_spec;apply Z.le_trans.
 Qed.
 
 Lemma ltb_trans : forall x y z, x < y = true ->  y < z = true -> x < z = true.
 Proof.
- intros x y z;rewrite !ltb_spec;apply Zlt_trans.
+ intros x y z;rewrite !ltb_spec;apply Z.lt_trans.
 Qed.
 
 Lemma ltb_leb_trans : forall x y z, x < y = true ->  y <= z = true -> x < z = true.
 Proof.
- intros x y z;rewrite leb_spec, !ltb_spec;apply Zlt_le_trans.
+ intros x y z;rewrite leb_spec, !ltb_spec;apply Z.lt_le_trans.
 Qed.
 
 Lemma leb_ltb_trans : forall x y z, x <= y = true ->  y < z = true -> x < z = true.
 Proof.
- intros x y z;rewrite leb_spec, !ltb_spec;apply Zle_lt_trans.
+ intros x y z;rewrite leb_spec, !ltb_spec;apply Z.le_lt_trans.
 Qed.
 
 Lemma gtb_not_leb : forall n m, m < n = true -> ~(n <= m = true).
@@ -1828,7 +1825,7 @@ Qed.
 
 Lemma leb_refl : forall n, n <= n = true.
 Proof.
- intros n;rewrite leb_spec;apply Zle_refl.
+ intros n;rewrite leb_spec;apply Z.le_refl.
 Qed.
 
 Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x).
@@ -2083,7 +2080,7 @@ Qed.
 (*   assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *)
 (*    apply Z.mod_pos_bound;auto with zarith. *)
 (*   change (2^1)%Z with 2%Z;split;try omega. *)
-(*   apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *)
+(*   apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *)
 (*   rewrite inj_S, Zpower_Zsucc;omega. *)
 (*   unfold wB;apply Zpower_le_monotone;auto with zarith. *)
 (*   split;auto using inj_le with zarith. *)
@@ -2100,7 +2097,7 @@ Qed.
 (*   assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *)
 (*    apply Z.mod_pos_bound;auto with zarith. *)
 (*   change (2^1)%Z with 2%Z;split;try omega. *)
-(*   apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *)
+(*   apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *)
 (*   rewrite inj_S, Zpower_Zsucc;omega. *)
 (*   unfold wB;apply Zpower_le_monotone;auto with zarith. *)
 (*   split;auto using inj_le with zarith. *)
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 543d6f0..e275b8f 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -33,7 +33,7 @@
 -I versions/standard/Int63
 -I versions/standard/Array
 
--I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
+# -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
 
 -extra "test" "" "cd ../unit-tests; make"
 -extra "ztest" "" "cd ../unit-tests; make zchaff"
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 74caf8b..f259a70 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -14,8 +14,95 @@ open Entries
 
 
 (* Constr generation and manipulation *)
+type id = Names.variable
+let mkId = Names.Id.of_string
+
+
+type name = Names.Name.t
+let name_of_id i = Names.Name i
+let mkName s =
+  let id = mkId s in
+  name_of_id id
+let string_of_name = function
+    Names.Name id -> Names.Id.to_string id
+  | _ -> failwith "unnamed rel"
+
+
+type constr = Constr.t
+type types = Constr.types
+let eq_constr = Constr.equal
+let hash_constr = Constr.hash
+let mkProp = Constr.mkProp
+let mkConst = Constr.mkConst
+let mkVar = Constr.mkVar
+let mkRel = Constr.mkRel
+let isRel = Constr.isRel
+let destRel = Constr.destRel
+let lift = Vars.lift
+let mkApp = Constr.mkApp
+let decompose_app = Constr.decompose_app
+let mkLambda = Constr.mkLambda
+let mkProd = Constr.mkProd
+let mkLetIn = Constr.mkLetIn
+
+let pr_constr_env env = Printer.pr_constr_env env Evd.empty
+let pr_constr = pr_constr_env Environ.empty_env
+
+
+let mkUConst : Constr.t -> 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 (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 (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
+    const_entry_universes   = Evd.const_univ_entry ~poly:false evd;
+    const_entry_opaque      = false;
+    const_entry_inline_code = false }
+
+let mkTConst c noc ty =
+  let env = Global.env () in
+  let evd = Evd.from_env env 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;
+    const_entry_feedback    = None;
+    const_entry_type        = Some ty;
+    const_entry_universes   = Evd.const_univ_entry ~poly:false evd;
+    const_entry_opaque      = false;
+    const_entry_inline_code = false }
+
+(* TODO : Set -> Type *)
+let declare_new_type t =
+  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make t) in
+  Constr.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 (EConstr.of_constr constr_t) in
+  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make v) in
+  Constr.mkVar v
 
-let mklApp f args = Term.mkApp (Lazy.force f, args)
+let declare_constant n c =
+  Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
+
+
+
+type cast_kind = Constr.cast_kind
+let vmcast = Constr.VMcast
+let mkCast = Constr.mkCast
+
+
+(* EConstr *)
+type econstr = EConstr.t
+let econstr_of_constr = EConstr.of_constr
+
+
+(* Modules *)
 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)
 
@@ -23,12 +110,13 @@ let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules
 (* Int63 *)
 let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]]
 
+(* 31-bits integers are "called" 63 bits (this is sound) *)
 let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]]
 let cD0 = gen_constant int31_module "D0"
 let cD1 = gen_constant int31_module "D1"
 let cI31 = gen_constant int31_module "I31"
 
-let mkInt : int -> Term.constr = fun i ->
+let mkInt : int -> constr = fun i ->
   let a = Array.make 31 (Lazy.force cD0) in
   let j = ref i in
   let k = ref 30 in
@@ -37,7 +125,7 @@ let mkInt : int -> Term.constr = fun i ->
     j := !j lsr 1;
     decr k
   done;
-  mklApp cI31 a
+  mkApp (Lazy.force cI31, a)
 
 let cint = gen_constant int31_module "int31"
 
@@ -49,7 +137,7 @@ let cmake = gen_constant parray_modules "make"
 let cset = gen_constant parray_modules "set"
 
 let max_array_size : int = 4194302
-let mkArray : Term.types * Term.constr array -> Term.constr =
+let mkArray : Constr.types * Constr.t array -> Constr.t =
   fun (ty, a) ->
   let l = (Array.length a) - 1 in
   snd (Array.fold_left (fun (i,acc) c ->
@@ -57,9 +145,9 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
                           if i = l then
                             acc
                           else
-                            mklApp cset [|ty; acc; mkInt i; c|] in
+                            mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in
                         (i+1,acc')
-                       ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a)
+                       ) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a)
 
 
 (* Traces *)
@@ -67,81 +155,37 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
 let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
   let rec mkTrace s =
     if s = size then
-      mklApp cnil [|step|]
+      mkApp (Lazy.force cnil, [|step|])
     else (
       r := next !r;
       let st = step_to_coq !r in
-      mklApp ccons [|step; st; mkTrace (s+1)|]
+      mkApp (Lazy.force ccons, [|step; st; mkTrace (s+1)|])
     ) in
-  mklApp cpair [|mklApp clist [|step|]; step; mkTrace 0; def_step|]
-
-
-(* Differences between the two versions of Coq *)
-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 (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 (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;
-    const_entry_inline_code = false }
-
-let mkTConst c noc ty =
-  let env = Global.env () in
-  let evd = Evd.from_env env 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;
-    const_entry_feedback    = None;
-    const_entry_type        = Some ty;
-    const_entry_polymorphic = false;
-    const_entry_universes   = snd (Evd.universe_context evd);
-    const_entry_opaque      = false;
-    const_entry_inline_code = false }
-
-let error s = CErrors.user_err (Pp.str s)
+  mkApp (Lazy.force cpair, [|mkApp (Lazy.force clist, [|step|]); step; mkTrace 0; def_step|])
 
-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 (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 (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 c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
-
-let vernacentries_interp expr =
-  Vernacentries.interp (None, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr))
-
-let pr_constr_env env = Printer.pr_constr_env env Evd.empty
+(* 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 lift = Vars.lift
+let micromega_coq_proofTerm =
+  (* Cannot contain evars *)
+  lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm)))
 
-let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
-                          Context.Rel.Declaration.get_type r
+let micromega_dump_proof_term p =
+  (* Cannot contain evars *)
+  EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p)
 
-let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst
 
+(* Tactics *)
+type tactic = unit Proofview.tactic
 let tclTHEN = Tacticals.New.tclTHEN
 let tclTHENLAST = Tacticals.New.tclTHENLAST
 let assert_before n c = Tactics.assert_before n (EConstr.of_constr c)
 
-let vm_conv = Vconv.vm_conv
 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))
 
 let mk_tactic tac =
   Proofview.Goal.nf_enter (fun gl ->
@@ -157,7 +201,21 @@ let set_evars_tac noc =
       let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in
       Proofview.Unsafe.tclEVARS sigma)
 
+
+(* Other differences between the two versions of Coq *)
+type constr_expr = Constrexpr.constr_expr
+let error s = CErrors.user_err (Pp.str s)
+
+let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
+
+let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
+                          Context.Rel.Declaration.get_type r
+
+(* Cannot contain evars since it comes from a Constr.t *)
+let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst |> EConstr.Unsafe.to_constr
+
 let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
+
 let constrextern_extern_constr c =
   let env = Global.env () in
   Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c)
@@ -166,30 +224,10 @@ 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 *)
+  (* Cannot contain evars since it comes from a Constr.t *)
   EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))
 
+let vm_conv = Vconv.vm_conv
 
-(* 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
+(* Cannot contain evars since it comes from a Constr.t *)
+let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t))
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 3d17203..3d6f6b2 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -10,74 +10,80 @@
 (**************************************************************************)
 
 
-(* 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
+
+(* Constr generation and manipulation *)
+type id = Names.variable
+val mkId : string -> id
+
+type name
+val name_of_id : id -> name
+val mkName : string -> name
+val string_of_name : name -> string
+
+type constr = Constr.t
+type types = constr
+val eq_constr : constr -> constr -> bool
+val hash_constr : constr -> int
+val mkProp : types
+val mkConst : Names.Constant.t -> constr
+val mkVar : id -> constr
+val mkRel : int -> constr
+val isRel : constr -> bool
+val destRel : constr -> int
+val lift : int -> constr -> constr
+val mkApp : constr * constr array -> constr
+val decompose_app : constr -> constr * constr list
+val mkLambda : name * types * constr -> constr
+val mkProd : name * types * types -> types
+val mkLetIn : name * constr * types * constr -> constr
+
+val pr_constr_env : Environ.env -> constr -> Pp.t
+val pr_constr : constr -> Pp.t
+
+val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
+val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val declare_new_type : id -> types
+val declare_new_variable : id -> types -> constr
+val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+
+type cast_kind
+val vmcast : cast_kind
+val mkCast : constr * cast_kind * constr -> constr
+
+
+(* EConstr *)
+type econstr = EConstr.t
+val econstr_of_constr : constr -> econstr
+
+
+(* Modules *)
+val gen_constant : string list list -> string -> constr lazy_t
+
 
 (* Int63 *)
 val int63_modules : string list list
-val int31_module : string list list
-val cD0 : Term.constr lazy_t
-val cD1 : Term.constr lazy_t
-val cI31 : Term.constr lazy_t
-val mkInt : int -> Term.constr
-val cint : Term.constr lazy_t
+val mkInt : int -> constr
+val cint : 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
+val mkArray : types * constr array -> constr
+
 
 (* Traces *)
 val mkTrace :
-  ('a -> Term.constr) ->
+  ('a -> constr) ->
   ('a -> 'a) ->
   'b ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  int -> Term.constr -> Term.constr -> 'a ref -> Term.constr
-
-(* Differences between the two versions of Coq *)
-val mkUConst :
-  Term.constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst :
-  Term.constr ->
-  Term.constr ->
-  Term.types -> Safe_typing.private_constants Entries.definition_entry
-val error : string -> 'a
-val coqtype : Term.types Future.computation
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.constr -> Term.constr
-val extern_constr : Term.constr -> Constrexpr.constr_expr
-val vernacentries_interp : Constrexpr.constr_expr -> unit
-val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
-val lift : int -> Constr.constr -> Constr.constr
-val destruct_rel_decl : Context.Rel.Declaration.t -> Names.Name.t * Constr.t
-val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr
-val tclTHEN :
-  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
-val tclTHENLAST :
-  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
-val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic
-
-val vm_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
-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
+  constr Lazy.t ->
+  constr Lazy.t ->
+  constr Lazy.t ->
+  constr Lazy.t ->
+  int -> constr -> constr -> 'a ref -> constr
 
 
 (* Micromega *)
@@ -86,15 +92,30 @@ 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
+val micromega_coq_proofTerm : constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
 
 
-(* Types in the Coq source code *)
+(* Tactics *)
 type tactic = unit Proofview.tactic
-type names_id = Names.Id.t
+val tclTHEN : tactic -> tactic -> tactic
+val tclTHENLAST : tactic -> tactic -> tactic
+val assert_before : name -> types -> tactic
+val vm_cast_no_check : constr -> tactic
+val mk_tactic : (Environ.env -> Evd.evar_map -> constr -> tactic) -> tactic
+val set_evars_tac : constr -> tactic
+
+
+(* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
+val error : string -> 'a
+val extern_constr : constr -> constr_expr
+val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr
+val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr
+val ppconstr_lsimpleconstr : Notation_term.tolerability
+val constrextern_extern_constr : constr -> constr_expr
+val get_rel_dec_name : Context.Rel.Declaration.t -> name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
 
-(* EConstr *)
-type econstr = EConstr.t
-val econstr_of_constr : Term.constr -> econstr
+val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function
+val cbv_vm : Environ.env -> constr -> types -> constr
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 11989c5..71b28a8 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -10,10 +10,6 @@
 (**************************************************************************)
 
 
-open Entries
-open Declare
-open Decl_kinds
-
 open CoqTerms
 open SmtForm
 open SmtCertif
@@ -168,7 +164,7 @@ let interp_roots first last =
     let h = if Form.is_pos l then ph else ph lxor 1 in
     try Hashtbl.find tbl h
     with Not_found ->
-      let p = Term.mkApp (Term.mkRel 1, [|mkInt (x+1)|]) in
+      let p = Structures.mkApp (Structures.mkRel 1, [|mkInt (x+1)|]) in
       let np = mklApp cnegb [|p|] in
       Hashtbl.add tbl ph p;
       Hashtbl.add tbl (ph lxor 1) np;
@@ -199,14 +195,14 @@ let parse_certif dimacs trace fdimacs ftrace =
   let _,first,last,reloc = import_cnf fdimacs in
   let d = make_roots first last in
   let ce1 = Structures.mkUConst d in
-  let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in
+  let _ = Structures.declare_constant dimacs ce1 in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
   let ce2 = Structures.mkUConst certif in
-  let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in
+  let _ = Structures.declare_constant trace ce2 in
   ()
 
 let cdimacs = gen_constant sat_checker_modules "dimacs"
@@ -226,36 +222,36 @@ let theorems interp name fdimacs ftrace =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in
-  let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in
+  let vtype = Term.mkArrow (Lazy.force cint) (Lazy.force cbool) in
   let theorem_type =
-    Term.mkProd (mkName "v", vtype, theorem_concl) in
+    Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in
   let theorem_proof_cast =
-    Term.mkCast (
-        Term.mkLetIn (mkName "d", d, Lazy.force cdimacs,
-        Term.mkLetIn (mkName "c", certif, Lazy.force ccertif,
-        Term.mkLambda (mkName "v", vtype,
+    Structures.mkCast (
+        Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs,
+        Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif,
+        Structures.mkLambda (Structures.mkName "v", vtype,
         mklApp ctheorem_checker
-               [| Term.mkRel 3(*d*); Term.mkRel 2(*c*);
+               [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*);
 		  vm_cast_true_no_check
-		    (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]);
-                  Term.mkRel 1(*v*)|]))),
-      Term.VMcast,
+		    (mklApp cchecker [|Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]);
+                  Structures.mkRel 1(*v*)|]))),
+      Structures.vmcast,
       theorem_type)
   in
   let theorem_proof_nocast =
-    Term.mkLetIn (mkName "d", d, Lazy.force cdimacs,
-    Term.mkLetIn (mkName "c", certif, Lazy.force ccertif,
-    Term.mkLambda (mkName "v", vtype,
+    Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs,
+    Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif,
+    Structures.mkLambda (Structures.mkName "v", vtype,
     mklApp ctheorem_checker
-           [| Term.mkRel 3(*d*); Term.mkRel 2(*c*)|])))
+           [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|])))
   in
   let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in
-  let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
+  let _ = Structures.declare_constant name ce in
   ()
 
 let theorem = theorems (fun _ -> interp_roots)
 let theorem_abs =
-  theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Term.mkRel 1(*v*)|]; d|])
+  theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Structures.mkRel 1(*v*)|]; d|])
 
 
 let checker fdimacs ftrace =
@@ -270,8 +266,11 @@ let checker fdimacs ftrace =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
   let tm = mklApp cchecker [|d; certif|] in
-  let expr = Structures.extern_constr tm in
-  Structures.vernacentries_interp expr
+
+  let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+  Format.eprintf "     = %s\n     : bool@."
+    (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then
+        "true" else "false")
 
 
 
@@ -359,22 +358,22 @@ let cchecker_eq_correct =
 let cchecker_eq = gen_constant cnf_checker_modules "checker_eq"
 
 let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
-  let ntvar = mkName "t_var" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
+  let ntvar = Structures.mkName "t_var" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
     SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
-  let vtvar = Term.mkRel 3 in
-  let vtform = Term.mkRel 2 in
-  let vc = Term.mkRel 1 in
+  let vtvar = Structures.mkRel 3 in
+  let vtform = Structures.mkRel 2 in
+  let vc = Structures.mkRel 1 in
   let add_lets t =
-    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Structures.mkLetIn (nc, certif, Lazy.force ccertif,
     t)))
   in
   let cbc =
@@ -392,22 +391,22 @@ let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
 
 
 let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast =
-  let ntvar = mkName "t_var" in
-  let ntform = mkName "t_form" in
-  let nc = mkName "c" in
+  let ntvar = Structures.mkName "t_var" in
+  let ntform = Structures.mkName "t_form" in
+  let nc = Structures.mkName "c" in
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
     SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
-  let vtvar = Term.mkRel 3 in
-  let vtform = Term.mkRel 2 in
-  let vc = Term.mkRel 1 in
+  let vtvar = Structures.mkRel 3 in
+  let vtform = Structures.mkRel 2 in
+  let vc = Structures.mkRel 1 in
   let add_lets t =
-    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Structures.mkLetIn (nc, certif, Lazy.force ccertif,
     t)))
   in
   let ceqc = add_lets (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])
@@ -422,10 +421,10 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast =
   (proof_cast, proof_nocast)
 
 let get_arguments concl =
-  let f, args = Term.decompose_app concl in
+  let f, args = Structures.decompose_app concl in
   match args with
-  | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b
-  | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
+  | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b
+  | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
   | _ -> failwith ("Zchaff.get_arguments :can only deal with equality over bool")
 
 
@@ -529,9 +528,9 @@ let core_tactic vm_cast env sigma concl =
   let reify_atom = Atom.create () in
   let reify_form = Form.create () in
   let (body_cast, body_nocast) =
-    if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
+    if ((Structures.eq_constr b (Lazy.force ctrue)) || (Structures.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.get reify_atom) reify_form a in
-      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let l' = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
       let atom_tbl = Atom.atom_tbl reify_atom in
       let pform_tbl = Form.pform_tbl reify_form in
       let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index 6314927..63cf772 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -11,9 +11,9 @@
 
 
 val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
-val parse_certif : Structures.names_id -> Structures.names_id -> string -> string -> unit
+val parse_certif : Structures.id -> Structures.id -> string -> string -> unit
 val checker : string -> string -> unit
-val theorem : Structures.names_id -> string -> string -> unit
-val theorem_abs : Structures.names_id -> string -> string -> unit
+val theorem : Structures.id -> string -> string -> unit
+val theorem_abs : Structures.id -> string -> string -> unit
 val tactic : unit -> Structures.tactic
 val tactic_no_check : unit -> Structures.tactic
-- 
cgit