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

7 files changed, 441 insertions, 317 deletions

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