More on the support for standard Coq (not working yet)

16 files changed, 139 insertions, 90 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 5f6120e..64e411c 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -14,7 +14,6 @@
 (**************************************************************************)
 
 
-Add LoadPath "." as SMTCoq.
 Require Import Bool List Int63 PArray.
 Require Import Misc State.
 
@@ -93,7 +92,7 @@ Module Form.
             t_b.[i <- interp_aux (PArray.get t_b) hf])
         (PArray.make (PArray.length t_form) true) t_form.
 
-      Fixpoint lt_form i h:=
+      Fixpoint lt_form i h {struct h} :=
         match h with
         | Fatom _ | Ftrue | Ffalse => true
         | Fnot2 _ l => Lit.blit l < i
@@ -180,7 +179,7 @@ Module Form.
       let t_interp := t_interp t_form in
       PArray.get t_interp.
 
-    Register interp_aux as PrimInline.
+    (* Register interp_aux as PrimInline. *)
     Definition interp t_form := interp_aux (interp_state_var t_form).
 
     Lemma wf_interp_form_lt :
diff --git a/src/State.v b/src/State.v
index d793410..0830ac6 100644
--- a/src/State.v
+++ b/src/State.v
@@ -41,7 +41,7 @@ End Valuation.
 Module Var.
 
   Definition _true : var := 0. (* true *)
-  Register _true as PrimInline.
+  (* Register _true as PrimInline. *)
 
   Definition _false : var := 1. (* false *)
 
@@ -60,34 +60,34 @@ Notation _lit := int (only parsing).
 Module Lit.
 
   Definition is_pos (l:_lit) := is_even l.
-  Register is_pos as PrimInline.
+  (* Register is_pos as PrimInline. *)
 
   Definition blit (l:_lit) : var := l >> 1.
-  Register blit as PrimInline.
+  (* Register blit as PrimInline. *)
 
   Definition lit (x:var) : _lit := x << 1.
-  Register lit as PrimInline.
+  (* Register lit as PrimInline. *)
 
   Definition neg (l:_lit) : _lit := l lxor 1.
-  Register neg as PrimInline.
+  (* Register neg as PrimInline. *)
 
   Definition nlit (x:var) : _lit := neg (lit x).
-  Register nlit as PrimInline.
+  (* Register nlit as PrimInline. *)
 
   Definition _true : _lit := Eval compute in lit Var._true.
-  Register _true as PrimInline.
+  (* Register _true as PrimInline. *)
 
   Lemma lit_true : _true = lit Var._true.
   Proof. reflexivity. Qed.
 
   Definition _false : _lit := Eval compute in lit Var._false.
-  Register _false as PrimInline.
+  (* Register _false as PrimInline. *)
 
   Lemma lit_false : _false = lit Var._false.
   Proof. reflexivity. Qed.
 
   Definition eqb (l l' : _lit) := l == l'.
-  Register eqb as PrimInline.
+  (* Register eqb as PrimInline. *)
 
   Lemma eqb_spec : forall l l', eqb l l' = true <-> l = l'.
   Proof eqb_spec.
@@ -435,12 +435,12 @@ Module S.
   Definition t := array C.t.
 
   Definition get (s:t) (cid:clause_id) := s.[cid].
-  Register get as PrimInline.
+  (* Register get as PrimInline. *)
 
   (* Do not use this function outside this module *)
   (* expect if you are sure that [c = sort_uniq c] *)
   Definition internal_set (s:t) (cid:clause_id) (c:C.t) : t := s.[cid <- c].
-  Register internal_set as PrimInline.
+  (* Register internal_set as PrimInline. *)
 
   Definition make (nclauses : int) : t :=
     PArray.make nclauses C._true.
@@ -474,7 +474,7 @@ Module S.
       forall c, C.valid rho c ->
         forall id, valid rho (set s id c).
   Proof.
-    unfold valid, get, set;simpl;intros.
+    unfold valid, get;simpl;intros.
     destruct (Int63Properties.reflect_eqb id id0);subst.
     case_eq (id0 < length s);intros.
     rewrite PArray.get_set_same;trivial.
diff --git a/src/Trace.v b/src/Trace.v
index d369958..7930a83 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -51,7 +51,7 @@ Section trace.
   Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool :=
     let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in
     is_false (S.get s' confl).
-  Register _checker_ as PrimInline.
+  (* Register _checker_ as PrimInline. *)
 
   (* For debugging *)
   (*
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index d918dab..fb70223 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -13,8 +13,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-Require Import PArray List Bool.
 (* Add LoadPath ".." as SMTCoq. *)
+Require Import PArray List Bool.
 Require Import Misc State SMT_terms.
 
 Import Form.
@@ -28,11 +28,11 @@ Unset Strict Implicit.
 Definition or_of_imp args :=
   let last := PArray.length args - 1 in
   PArray.mapi (fun i l => if i == last then l else Lit.neg l) args.
-Register or_of_imp as PrimInline.
+(* Register or_of_imp as PrimInline. *)
 
 Lemma length_or_of_imp : forall args,
   PArray.length (or_of_imp args) = PArray.length args.
-Proof. intro; apply length_mapi. Qed.
+Proof. intro; unfold or_of_imp; apply length_mapi. Qed.
 
 Lemma get_or_of_imp : forall args i,
   i < (PArray.length args) - 1 -> (or_of_imp args).[i] = Lit.neg (args.[i]).
@@ -271,7 +271,7 @@ Section CHECKER.
 
   Lemma valid_check_False : C.valid rho check_False.
   Proof.
-    unfold check_False, C.valid;simpl.
+    unfold check_False, C.valid. change (Lit.interp rho (Lit.neg Lit._false) || false = true).
     rewrite Lit.interp_neg.
     assert (W:= Lit.interp_false _ Hwfrho).
     destruct (Lit.interp rho Lit._false);trivial;elim W;red;trivial.
diff --git a/src/euf/Euf.v b/src/euf/Euf.v
index 9b86bf3..e3d73f6 100644
--- a/src/euf/Euf.v
+++ b/src/euf/Euf.v
@@ -36,7 +36,7 @@ Section certif.
       end
     | _ => C._true
     end.
-  Register get_eq as PrimInline.
+  (* Register get_eq as PrimInline. *)
 
   Fixpoint check_trans_aux (t1 t2:int)
       (eqs:list _lit) (res:_lit) (clause:C.t) : C.t :=
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index 0969db0..282523a 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -21,7 +21,6 @@ Require Import RingMicromega.
 Require Import ZMicromega.
 Require Import Tauto.
 Require Import Psatz.
-(* Add LoadPath ".." as SMTCoq. *)
 
 Require Import Misc State.
 Require Import SMT_terms.
@@ -40,7 +39,7 @@ Section certif.
 
   Import EnvRing Atom.
 
-  Register option_map as PrimInline.
+  (* Register option_map as PrimInline. *)
 
   Section BuildPositive.
     Variable build_positive : hatom -> option positive.
@@ -62,7 +61,7 @@ Section certif.
       (PArray.length t_atom) 0 (fun _ => None).
 
   Definition build_positive_atom := build_positive_atom_aux build_positive.
-  Register build_positive_atom as PrimInline.
+  (* Register build_positive_atom as PrimInline. *)
 
   Section BuildZ.
 
@@ -321,7 +320,7 @@ Section certif.
         | _ => C._true
       end
       else C._true.
-  Register get_eq as PrimInline.
+  (* Register get_eq as PrimInline. *)
 
   Definition get_not_le (l:_lit) (f : Atom.hatom -> Atom.hatom -> C.t) :=
     if negb (Lit.is_pos l) then
@@ -334,7 +333,7 @@ Section certif.
       | _ => C._true
     end
       else C._true.
-  Register get_not_le as PrimInline.
+  (* Register get_not_le as PrimInline. *)
 
   Definition check_micromega cl c : C.t :=
     match build_clause empty_vmap cl with
diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v
index d7d2594..e0ef14e 100644
--- a/src/spl/Syntactic.v
+++ b/src/spl/Syntactic.v
@@ -282,7 +282,7 @@ Section FLATTEN.
       | Some a => PArray.fold_left frec largs a
       | None => l::largs
     end.
-  Register flatten_op_body as PrimInline.
+  (* Register flatten_op_body as PrimInline. *)
 
 
   Definition flatten_op_lit (get_op:_lit -> option (array _lit)) max :=
@@ -331,7 +331,7 @@ Section FLATTEN.
                 | Fatom a1, Fatom a2 => check_neg_atom a1 a2
                 | _, _ => false (* We maybe need to extend the rule here ... *)
               end.
-  Register check_flatten_body as PrimInline.
+  (* Register check_flatten_body as PrimInline. *)
 
   Definition check_flatten_aux l lf :=
     foldi_cont (fun _ => check_flatten_body) 0 (PArray.length t_form) (fun _ _ => false) l lf.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index d71ba45..e8a7737 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -18,7 +18,7 @@ open Coqlib
 let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 (* Int63 *)
-let cint = gen_constant Structures.int63_modules "int"
+let cint = Structures.cint
 let ceq63 = gen_constant Structures.int63_modules "eqb"
 
 (* PArray *)
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index de2879c..26edef3 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -17,12 +17,18 @@
 open Entries
 
 
+
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+
+
+
 (* Int63 *)
 let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
 
 let mkInt : int -> Term.constr =
   fun i -> Term.mkInt (Uint63.of_int i)
 
+let cint = gen_constant Structures.int63_modules "int"
 
 (* PArray *)
 let parray_modules = [["Coq";"Array";"PArray"]]
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index ddbe0ab..069c159 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -19,9 +19,11 @@
    trees *)
 
 
+Require Import Int31.
 Require Export Int63.
-Require Import Ring63.
-Require Int63Lib.
+(* Require Export Int63. *)
+(* Require Import Ring63. *)
+(* Require Int63Lib. *)
 Require FMapAVL.
 
 Local Open Scope int63_scope.
@@ -87,7 +89,7 @@ Local Open Scope array_scope.
 
 Set Vm Optimize.
 
-Definition max_array_length := Eval vm_compute in (Int63Lib.phi_inv 4194302).
+Definition max_array_length := 4194302%int31.
 
 (** Axioms *)
 Axiom get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index 6a002ea..ed0fe18 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -17,7 +17,8 @@
 
 Require Import Bvector.
 Require Export BigNumPrelude.
-Require Import Int63Lib.
+(* Require Import Int63Lib. *)
+Require Import Int31.
 Require Export Int63Native.
 Require Export Int63Op.
 
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v
index ada4821..6224e34 100644
--- a/src/versions/standard/Int63/Int63Native_standard.v
+++ b/src/versions/standard/Int63/Int63Native_standard.v
@@ -17,22 +17,23 @@
 
 (* Add LoadPath "." as SMTCoq.Int63.standard.versions. *)
 Require Export DoubleType.
-Require Import Int63Lib Cyclic63 Ring63.
+Require Import Int31 Cyclic31 Ring31.
 Require Import ZArith.
 Require Import Bool.
 
 
 Definition size := size.
 
-Notation int := int63.
+Notation int := int31.
 
 Delimit Scope int63_scope with int.
 Bind Scope int63_scope with int.
 
 (* Some constants *)
-Notation "0" := On : int63_scope.
-Notation "1" := In : int63_scope.
-Notation "2" := Twon : int63_scope.
+Notation "0" := 0%int31 : int63_scope.
+Notation "1" := 1%int31 : int63_scope.
+Notation "2" := 2%int31 : int63_scope.
+Notation "3" := 3%int31 : int63_scope.
 
 (* Logical operations *)
 Definition lsl : int -> int -> int :=
@@ -43,61 +44,76 @@ Definition lsr : int -> int -> int :=
   fun i j => nshiftr (N.to_nat (Z.to_N (phi j))) i.
 Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
 
+(* For the bitwise operations, I add a useless pattern matching to avoid
+   too much unfolding of their definitions at Qed (since Qed bypasses
+   the Opaque declaration) *)
 Definition land : int -> int -> int :=
-  fun i j =>
-    recrter _ j (fun d _ acc =>
+  fun i => match i with
+  | 0%int31 | _ => fun j =>
+    recrbis _ j (fun d _ acc =>
                    let r := acc in
                    let d' := firstl r in
                    let dr := match d, d' with | D1, D1 => D1 | _, _ => D0 end in
                    sneakl dr r
-                ) i.
+                ) i
+           end.
+Global Arguments land i j : simpl never.
+Global Opaque land.
 Infix "land" := land (at level 40, left associativity) : int63_scope.
 
 Definition lor : int -> int -> int :=
-  fun i j =>
-    recrter _ j (fun d _ acc =>
+  fun i => match i with
+  | 0%int31 | _ => fun j =>
+    recrbis _ j (fun d _ acc =>
                    let r := acc in
                    let d' := firstl r in
                    let dr := match d, d' with | D0, D0 => D0 | _, _ => D1 end in
                    sneakl dr r
-                ) i.
+                ) i
+           end.
+Global Arguments lor i j : simpl never.
+Global Opaque lor.
 Infix "lor" := lor (at level 40, left associativity) : int63_scope.
 
 Definition lxor : int -> int -> int :=
-  fun i j =>
-    recrter _ j (fun d _ acc =>
+  fun i => match i with
+  | 0%int31 | _ => fun j =>
+    recrbis _ j (fun d _ acc =>
                    let r := acc in
                    let d' := firstl r in
                    let dr := match d, d' with | D0, D0 | D1, D1 => D0 | _, _ => D1 end in
                    sneakl dr r
-                ) i.
+                ) i
+           end.
+Global Arguments lxor i j : simpl never.
+Global Opaque lxor.
 Infix "lxor" := lxor (at level 40, left associativity) : int63_scope.
 
 (* Arithmetic modulo operations *)
 (* Definition add : int -> int -> int := add63. *)
 (* Notation "n + m" := (add n m) : int63_scope. *)
-Notation "n + m" := (add63 n m) : int63_scope.
+Notation "n + m" := (add31 n m) : int63_scope.
 
 (* Definition sub : int -> int -> int := sub63. *)
 (* Notation "n - m" := (sub n m) : int63_scope. *)
-Notation "n - m" := (sub63 n m) : int63_scope.
+Notation "n - m" := (sub31 n m) : int63_scope.
 
 (* Definition mul : int -> int -> int := mul63. *)
 (* Notation "n * m" := (mul n m) : int63_scope. *)
-Notation "n * m" := (mul63 n m) : int63_scope.
+Notation "n * m" := (mul31 n m) : int63_scope.
 
 Definition mulc : int -> int -> int * int :=
-  fun i j => match mul63c i j with
+  fun i j => match mul31c i j with
                | W0 => (0%int, 0%int)
                | WW h l => (h, l)
              end.
 
 Definition div : int -> int -> int :=
-  fun i j => let (q,_) := div63 i j in q.
+  fun i j => let (q,_) := div31 i j in q.
 Notation "n / m" := (div n m) : int63_scope.
 
 Definition modulo : int -> int -> int :=
-  fun i j => let (_,r) := div63 i j in r.
+  fun i j => let (_,r) := div31 i j in r.
 Notation "n '\%' m" := (modulo n m) (at level 40, left associativity) : int63_scope.
 
 (* Comparisons *)
@@ -113,15 +129,15 @@ Notation "n '\%' m" := (modulo n m) (at level 40, left associativity) : int63_sc
 (*     | I63 d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19 d20 d21 d22 d23 d24 d25 d26 d27 d28 d29 d30 d31 d32 d33 d34 d35 d36 d37 d38 d39 d40 d41 d42 d43 d44 d45 d46 d47 d48 d49 d50 d51 d52 d53 d54 d55 d56 d57 d58 d59 d60 d61 d62, I63 d'0 d'1 d'2 d'3 d'4 d'5 d'6 d'7 d'8 d'9 d'10 d'11 d'12 d'13 d'14 d'15 d'16 d'17 d'18 d'19 d'20 d'21 d'22 d'23 d'24 d'25 d'26 d'27 d'28 d'29 d'30 d'31 d'32 d'33 d'34 d'35 d'36 d'37 d'38 d'39 d'40 d'41 d'42 d'43 d'44 d'45 d'46 d'47 d'48 d'49 d'50 d'51 d'52 d'53 d'54 d'55 d'56 d'57 d'58 d'59 d'60 d'61 d'62 => *)
 (*       (eqb_digits d0 d'0) && (eqb_digits d1 d'1) && (eqb_digits d2 d'2) && (eqb_digits d3 d'3) && (eqb_digits d4 d'4) && (eqb_digits d5 d'5) && (eqb_digits d6 d'6) && (eqb_digits d7 d'7) && (eqb_digits d8 d'8) && (eqb_digits d9 d'9) && (eqb_digits d10 d'10) && (eqb_digits d11 d'11) && (eqb_digits d12 d'12) && (eqb_digits d13 d'13) && (eqb_digits d14 d'14) && (eqb_digits d15 d'15) && (eqb_digits d16 d'16) && (eqb_digits d17 d'17) && (eqb_digits d18 d'18) && (eqb_digits d19 d'19) && (eqb_digits d20 d'20) && (eqb_digits d21 d'21) && (eqb_digits d22 d'22) && (eqb_digits d23 d'23) && (eqb_digits d24 d'24) && (eqb_digits d25 d'25) && (eqb_digits d26 d'26) && (eqb_digits d27 d'27) && (eqb_digits d28 d'28) && (eqb_digits d29 d'29) && (eqb_digits d30 d'30) && (eqb_digits d31 d'31) && (eqb_digits d32 d'32) && (eqb_digits d33 d'33) && (eqb_digits d34 d'34) && (eqb_digits d35 d'35) && (eqb_digits d36 d'36) && (eqb_digits d37 d'37) && (eqb_digits d38 d'38) && (eqb_digits d39 d'39) && (eqb_digits d40 d'40) && (eqb_digits d41 d'41) && (eqb_digits d42 d'42) && (eqb_digits d43 d'43) && (eqb_digits d44 d'44) && (eqb_digits d45 d'45) && (eqb_digits d46 d'46) && (eqb_digits d47 d'47) && (eqb_digits d48 d'48) && (eqb_digits d49 d'49) && (eqb_digits d50 d'50) && (eqb_digits d51 d'51) && (eqb_digits d52 d'52) && (eqb_digits d53 d'53) && (eqb_digits d54 d'54) && (eqb_digits d55 d'55) && (eqb_digits d56 d'56) && (eqb_digits d57 d'57) && (eqb_digits d58 d'58) && (eqb_digits d59 d'59) && (eqb_digits d60 d'60) && (eqb_digits d61 d'61) && (eqb_digits d62 d'62) *)
 (*   end. *)
-Definition eqb := eqb63.
+Definition eqb := eqb31.
 Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
 
 Definition ltb : int -> int -> bool :=
-  fun i j => match compare63 i j with | Lt => true | _ => false end.
+  fun i j => match compare31 i j with | Lt => true | _ => false end.
 Notation "m < n" := (ltb m n) : int63_scope.
 
 Definition leb : int -> int -> bool :=
-  fun i j => match compare63 i j with | Gt => false | _ => true end.
+  fun i j => match compare31 i j with | Gt => false | _ => true end.
 Notation "m <= n" := (leb m n) : int63_scope.
 
 (* This operator has the following reduction rule
@@ -153,7 +169,7 @@ Definition foldi_cont
   if ltb to from then
     cont
   else
-    let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * (A -> B))%type) =>
+    let (_,r) := iter_int31 (to - from) _ (fun (jy: (int * (A -> B))%type) =>
                      let (j,y) := jy in ((j+1)%int, f j y)
                                       ) (from, cont) in
     f to r.
@@ -166,7 +182,7 @@ Definition foldi_down_cont
   if ltb from downto then
     cont
   else
-    let (_,r) := iter_int63 (from - downto) _ (fun (jy: (int * (A -> B))%type) =>
+    let (_,r) := iter_int31 (from - downto) _ (fun (jy: (int * (A -> B))%type) =>
                      let (j,y) := jy in ((j-1)%int, f j y)
                                       ) (from, cont) in
     f downto r.
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
index 119e6bd..1863497 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -15,7 +15,7 @@
 (**************************************************************************)
 
 
-Require Import Int63Lib Cyclic63.
+Require Import Int31 Cyclic31.
 Require Export Int63Native.
 Require Import BigNumPrelude.
 Require Import Bvector.
@@ -24,7 +24,7 @@ Require Import Bvector.
 Local Open Scope int63_scope.
 
 (** The number of digits as a int *)
-Definition digits := zdigits.
+Definition digits := 31%int31.
 
 (** The bigger int *)
 Definition max_int := Eval vm_compute in 0 - 1.
@@ -69,36 +69,36 @@ Definition addc_def x y :=
   let r := x + y in
   if r < x then C1 r else C0 r.
 (* the same but direct implementation for efficiancy *)
-Definition addc : int -> int -> carry int := add63c.
+Definition addc : int -> int -> carry int := add31c.
 Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
 
 Definition addcarryc_def x y :=
   let r := addcarry x y in
   if r <= x then C1 r else C0 r.
 (* the same but direct implementation for efficiancy *)
-Definition addcarryc : int -> int -> carry int := add63carryc.
+Definition addcarryc : int -> int -> carry int := add31carryc.
 
 Definition subc_def x y :=
   if y <= x then C0 (x - y) else C1 (x - y).
 (* the same but direct implementation for efficiancy *)
-Definition subc : int -> int -> carry int := sub63c.
+Definition subc : int -> int -> carry int := sub31c.
 Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
 
 Definition subcarryc_def x y :=
   if y < x then C0 (x - y - 1) else C1 (x - y - 1).
 (* the same but direct implementation for efficiancy *)
-Definition subcarryc : int -> int -> carry int := sub63carryc.
+Definition subcarryc : int -> int -> carry int := sub31carryc.
 
 Definition diveucl_def x y := (x/y, x\%y).
 (* the same but direct implementation for efficiancy *)
-Definition diveucl : int -> int -> int * int := div63.
+Definition diveucl : int -> int -> int * int := div31.
 
-Definition diveucl_21 : int -> int -> int -> int * int := div6321.
+Definition diveucl_21 : int -> int -> int -> int * int := div3121.
 
 Definition addmuldiv_def p x y :=
   (x << p) lor (y >> (digits - p)).
 (* the same but direct implementation for efficiancy *)
-Definition addmuldiv : int -> int -> int -> int := addmuldiv63.
+Definition addmuldiv : int -> int -> int -> int := addmuldiv31.
 
 Definition oppc (i:int) := 0 -c i.
 
@@ -111,14 +111,14 @@ Definition compare_def x y :=
   if x < y then Lt
   else if (x == y) then Eq else Gt.
 
-Definition compare : int -> int -> comparison := compare63.
+Definition compare : int -> int -> comparison := compare31.
 Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope.
 
 (** Exotic operations *)
 
 (** I should add the definition (like for compare) *)
-Definition head0 : int -> int := head063.
-Definition tail0 : int -> int := tail063.
+Definition head0 : int -> int := head031.
+Definition tail0 : int -> int := tail031.
 
 (** Iterators *)
 
@@ -183,7 +183,7 @@ Definition gcd := gcd_rec (2*size).
 
 Definition sqrt_step (rec: int -> int -> int) (i j: int)  :=
   let quo := i/j in
-  if quo < j then rec i ((j + i/j) >> 1)
+  if quo < j then rec i ((j + (i/j)%int) >> 1)
   else j.
 
 Definition iter_sqrt :=
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index e61714a..ccb103b 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -17,7 +17,8 @@
 
 Require Import Zgcd_alt.
 Require Import Bvector.
-Require Import Int63Lib Cyclic63.
+(* Require Import Int63Lib Cyclic63. *)
+Require Import Int31 Cyclic31.
 Require Export Int63Axioms.
 Require Import Eqdep_dec.
 Require Import Psatz.
@@ -285,7 +286,7 @@ Qed.
 
 Lemma opp_spec : forall x : int, [|- x|] = - [|x|] mod wB.
 Proof.
- unfold opp;intros;rewrite sub_spec, to_Z_0;trivial.
+ unfold opp;intros. rewrite sub_spec, to_Z_0;trivial.
 Qed.
 
 Lemma oppcarry_spec : forall x, [|oppcarry x|] = wB - [|x|] - 1.
@@ -405,7 +406,7 @@ Proof.
  unfold sqrt_step.
  case_eq ((i / j < j)%int);[ | rewrite <- Bool.not_true_iff_false];
   rewrite ltb_spec, div_spec;intros.
- assert ([| j + i / j|] = [|j|] + [|i|]/[|j|]).
+ assert ([| j + (i / j)%int|] = [|j|] + [|i|]/[|j|]).
    rewrite add_spec, Zmod_small;rewrite div_spec;auto with zarith.
  apply Hrec;rewrite lsr_spec, H0, to_Z_1;change (2^1) with 2.
  split; [ | apply sqrt_test_false;auto with zarith].
@@ -429,11 +430,11 @@ Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
   [|iter_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter_sqrt n rec i j|] + 1) ^ 2.
 Proof.
  revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n.
- intros rec i j Hi Hj Hij H31 Hrec. replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add63 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add63 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2) by reflexivity. apply sqrt_step_correct; auto with zarith.
+ intros rec i j Hi Hj Hij H31 Hrec. replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add31 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add31 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2) by reflexivity. apply sqrt_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec i j Hi Hj Hij H31 HHrec.
- replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add63 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add63 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] ^ 2 <= [|i|] < ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] + 1) ^ 2) by reflexivity.
+ replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add31 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add31 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] ^ 2 <= [|i|] < ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] + 1) ^ 2) by reflexivity.
  apply sqrt_step_correct; auto.
  intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
  intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith.
@@ -775,7 +776,7 @@ Proof.
  unfold Zgcd_bound.
  generalize (to_Z_bounded b).
  destruct [|b|].
- unfold size; intros _; change Int63Lib.size with 63%nat; omega.
+ unfold size; intros _; change Int31.size with 31%nat; omega.
  intros (_,H).
  cut (Psize p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto].
  intros (H,_); compute in H; elim H; auto.
@@ -903,7 +904,7 @@ Proof.
 Qed.
 
 
-Coercion b2i (b: bool) : int63 := if b then 1%int else 0%int.
+Coercion b2i (b: bool) : int := if b then 1%int else 0%int.
 
 Lemma bit_0 n : bit 0 n = false.
 Proof. unfold bit; rewrite lsr_0_l; auto. Qed.
@@ -1011,7 +1012,7 @@ Proof.
  intros n IH i1 i2 H1i1 H2i1 H1i2 H2i2 H.
  rewrite (bit_split i1), (bit_split i2).
  rewrite H.
- apply f_equal2 with (f := add63); auto.
+ apply f_equal2 with (f := add31); auto.
  apply f_equal2 with (f := lsl); auto.
  apply IH; try rewrite lsr_spec;
    replace (2^[|1|]) with 2%Z;  auto with zarith.
@@ -1477,8 +1478,8 @@ Proof.
  2: generalize (Hn 0%int); do 2 case bit; auto; intros [ ]; auto.
  rewrite lsl_add_distr.
  rewrite (bit_split x) at 1; rewrite (bit_split y) at 1.
- rewrite <-!add_assoc; apply f_equal2 with (f := add63); auto.
- rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add63); auto.
+ rewrite <-!add_assoc; apply f_equal2 with (f := add31); auto.
+ rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add31); auto.
  rewrite add_comm; auto.
  intros Heq.
  generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb.
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
index 1499dd3..52be2c3 100644
--- a/src/versions/standard/Int63/Int63_standard.v
+++ b/src/versions/standard/Int63/Int63_standard.v
@@ -18,8 +18,8 @@
 (** Naive software representation of Int63. To improve. Anyway, if you
     want efficiency, rather use native-coq. **)
 
-Require Export Cyclic63.
-Require Export Ring63.
+(* Require Export Cyclic31. *)
+Require Export Ring31.
 Require Export Int63Native.
 Require Export Int63Op.
 Require Export Int63Axioms.
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 6c95ffe..ae3157b 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -15,22 +15,47 @@
 
 
 open Entries
+open Coqlib
+
+
+let mklApp f args = Term.mkApp (Lazy.force f, args)
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 
 (* Int63 *)
-let int63_modules = [["SMTCoq";"Int63Native"]]
+let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]]
 
-let mkInt : int -> Term.constr =
-  failwith "Not implemented yet"
+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 a = Array.make 31 (Lazy.force cD0) in
+  let j = ref i in
+  let k = ref 30 in
+  while !j <> 0 do
+    if !j land 1 = 1 then a.(!k) <- Lazy.force cD1;
+    j := !j lsr 1;
+    decr k
+  done;
+  mklApp cI31 a
+
+let cint = gen_constant int31_module "int31"
 
 (* PArray *)
-let parray_modules = [["SMTCoq";"PArray"]]
+let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
+
+let cmake = gen_constant parray_modules "make"
+let cset = gen_constant parray_modules "set"
 
-let max_array_size : int =
-  failwith "Not implemented yet"
+let max_array_size : int = 4194302
 let mkArray : Term.types * Term.constr array -> Term.constr =
-  failwith "Not implemented yet"
+  fun (ty, a) ->
+  snd (Array.fold_left (fun (i,acc) c ->
+                        let acc' = mklApp cset [|ty; acc; mkInt i; c|] in
+                        (i+1,acc')
+                       ) (0,mklApp cmake [|ty; mkInt (Array.length a); a.(0)|]) a)
 
 
 (* Differences between the two versions of Coq *)