From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v   |   4 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v  |  80 ++--
 .../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v     | 425 ++++++++++-----------
 theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v   | 122 +++---
 theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 130 +++----
 theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v  |  38 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v   |  23 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v  |  29 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v   |   4 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v  |   6 +-
 10 files changed, 376 insertions(+), 485 deletions(-)

(limited to 'theories/Numbers/Cyclic/DoubleCyclic')

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index 305d77a9..deb216dd 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 3d44f96b..e6c5a0e0 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,16 +8,16 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 
 Local Open Scope Z_scope.
 
+Local Infix "<<" := Pos.shiftl_nat (at level 30).
+
 Section DoubleBase.
  Variable w : Type.
  Variable w_0   : w.
@@ -70,13 +70,7 @@ Section DoubleBase.
      end
   end.
 
- Fixpoint double_digits (n:nat) : positive :=
-  match n with
-  | O => w_digits
-  | S n => xO (double_digits n)
-  end.
-
- Definition double_wB n := base (double_digits n).
+ Definition double_wB n := base (w_digits << n).
 
  Fixpoint double_to_Z (n:nat) : word w n -> Z :=
   match n return word w n -> Z with
@@ -167,11 +161,7 @@ Section DoubleBase.
   Variable spec_w_0W  : forall l, [[w_0W l]] = [|l|].
   Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
   Variable spec_w_compare : forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+     w_compare x y = Zcompare [|x|] [|y|].
 
   Lemma wwB_wBwB : wwB = wB^2.
   Proof.
@@ -297,11 +287,10 @@ Section DoubleBase.
   Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n).
   Proof.
    intros n;unfold double_wB;simpl.
-   unfold base;rewrite (Zpos_xO (double_digits n)).
-   replace  (2 * Zpos (double_digits n)) with
-     (Zpos (double_digits n) + Zpos (double_digits n)).
+   unfold base. rewrite Pshiftl_nat_S, (Zpos_xO (_ << _)).
+   replace  (2 * Zpos (w_digits << n)) with
+     (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring.
    symmetry; apply Zpower_exp;intro;discriminate.
-   ring.
   Qed.
 
   Lemma double_wB_pos:
@@ -315,7 +304,7 @@ Section DoubleBase.
   Proof.
   clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1.
   intros n; elim n; clear n; auto.
-    unfold double_wB, double_digits; auto with zarith.
+    unfold double_wB, "<<"; auto with zarith.
   intros n H1; rewrite <- double_wB_wwB.
   apply Zle_trans with (wB * 1).
     rewrite Zmult_1_r; apply Zle_refl.
@@ -408,35 +397,40 @@ Section DoubleBase.
    intros a b c d H1; apply beta_lex_inv with (1 := H1); auto.
   Qed.
 
+  Ltac comp2ord := match goal with
+   | |- Lt = (?x ?= ?y) => symmetry; change (x < y)
+   | |- Gt = (?x ?= ?y) => symmetry; change (x > y); apply Zlt_gt
+  end.
+
   Lemma spec_ww_compare : forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+    ww_compare x y = Zcompare [[x]] [[y]].
   Proof.
    destruct x as [ |xh xl];destruct y as [ |yh yl];simpl;trivial.
-   generalize (spec_w_compare w_0 yh);destruct (w_compare w_0 yh);
-    intros H;rewrite spec_w_0 in H.
-   rewrite <- H;simpl;rewrite <- spec_w_0;apply spec_w_compare.
-   change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0.
+   (* 1st case *)
+   rewrite 2 spec_w_compare, spec_w_0.
+   destruct (Zcompare_spec 0 [|yh|]) as [H|H|H].
+   rewrite <- H;simpl. reflexivity.
+   symmetry. change (0 < [|yh|]*wB+[|yl|]).
+   change 0 with (0*wB+0). rewrite <- spec_w_0 at 2.
    apply wB_lex_inv;trivial.
-   absurd (0 <= [|yh|]). apply Zgt_not_le;trivial.
+   absurd (0 <= [|yh|]). apply Zlt_not_le; trivial.
    destruct (spec_to_Z yh);trivial.
-   generalize (spec_w_compare xh w_0);destruct (w_compare xh w_0);
-    intros H;rewrite spec_w_0 in H.
-   rewrite H;simpl;rewrite <- spec_w_0;apply spec_w_compare.
-   absurd (0 <= [|xh|]). apply Zgt_not_le;apply Zlt_gt;trivial.
+   (* 2nd case *)
+   rewrite 2 spec_w_compare, spec_w_0.
+   destruct (Zcompare_spec [|xh|] 0) as [H|H|H].
+   rewrite H;simpl;reflexivity.
+   absurd (0 <= [|xh|]). apply Zlt_not_le; trivial.
    destruct (spec_to_Z xh);trivial.
-   apply Zlt_gt;change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0.
-   apply wB_lex_inv;apply Zgt_lt;trivial.
-
-   generalize (spec_w_compare xh yh);destruct (w_compare xh yh);intros H.
-   rewrite H;generalize (spec_w_compare xl yl);destruct (w_compare xl yl);
-   intros H1;[rewrite H1|apply Zplus_lt_compat_l|apply Zplus_gt_compat_l];
-   trivial.
+   comp2ord.
+   change 0 with (0*wB+0). rewrite <- spec_w_0 at 2.
    apply wB_lex_inv;trivial.
-   apply Zlt_gt;apply wB_lex_inv;apply Zgt_lt;trivial.
+   (* 3rd case *)
+   rewrite 2 spec_w_compare.
+   destruct (Zcompare_spec [|xh|] [|yh|]) as [H|H|H].
+   rewrite H.
+   symmetry. apply Zcompare_plus_compat.
+   comp2ord. apply wB_lex_inv;trivial.
+   comp2ord. apply wB_lex_inv;trivial.
   Qed.
 
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 006da1b3..00a84052 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleCyclic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -30,65 +28,65 @@ Local Open Scope Z_scope.
 
 Section Z_2nZ.
 
- Variable w : Type.
- Variable w_op : znz_op w.
- Let w_digits      := w_op.(znz_digits).
- Let w_zdigits      := w_op.(znz_zdigits).
+ Context {t : Type}{ops : ZnZ.Ops t}.
+
+ Let w_digits      := ZnZ.digits.
+ Let w_zdigits      := ZnZ.zdigits.
 
- Let w_to_Z        := w_op.(znz_to_Z).
- Let w_of_pos      := w_op.(znz_of_pos).
- Let w_head0       := w_op.(znz_head0).
- Let w_tail0       := w_op.(znz_tail0).
+ Let w_to_Z        := ZnZ.to_Z.
+ Let w_of_pos      := ZnZ.of_pos.
+ Let w_head0       := ZnZ.head0.
+ Let w_tail0       := ZnZ.tail0.
 
- Let w_0            := w_op.(znz_0).
- Let w_1            := w_op.(znz_1).
- Let w_Bm1          := w_op.(znz_Bm1).
+ Let w_0            := ZnZ.zero.
+ Let w_1            := ZnZ.one.
+ Let w_Bm1          := ZnZ.minus_one.
 
- Let w_compare     := w_op.(znz_compare).
- Let w_eq0         := w_op.(znz_eq0).
+ Let w_compare     := ZnZ.compare.
+ Let w_eq0         := ZnZ.eq0.
 
- Let w_opp_c       := w_op.(znz_opp_c).
- Let w_opp         := w_op.(znz_opp).
- Let w_opp_carry   := w_op.(znz_opp_carry).
+ Let w_opp_c       := ZnZ.opp_c.
+ Let w_opp         := ZnZ.opp.
+ Let w_opp_carry   := ZnZ.opp_carry.
 
- Let w_succ_c      := w_op.(znz_succ_c).
- Let w_add_c       := w_op.(znz_add_c).
- Let w_add_carry_c := w_op.(znz_add_carry_c).
- Let w_succ        := w_op.(znz_succ).
- Let w_add         := w_op.(znz_add).
- Let w_add_carry   := w_op.(znz_add_carry).
+ Let w_succ_c      := ZnZ.succ_c.
+ Let w_add_c       := ZnZ.add_c.
+ Let w_add_carry_c := ZnZ.add_carry_c.
+ Let w_succ        := ZnZ.succ.
+ Let w_add         := ZnZ.add.
+ Let w_add_carry   := ZnZ.add_carry.
 
- Let w_pred_c      := w_op.(znz_pred_c).
- Let w_sub_c       := w_op.(znz_sub_c).
- Let w_sub_carry_c := w_op.(znz_sub_carry_c).
- Let w_pred        := w_op.(znz_pred).
- Let w_sub         := w_op.(znz_sub).
- Let w_sub_carry   := w_op.(znz_sub_carry).
+ Let w_pred_c      := ZnZ.pred_c.
+ Let w_sub_c       := ZnZ.sub_c.
+ Let w_sub_carry_c := ZnZ.sub_carry_c.
+ Let w_pred        := ZnZ.pred.
+ Let w_sub         := ZnZ.sub.
+ Let w_sub_carry   := ZnZ.sub_carry.
 
 
- Let w_mul_c       := w_op.(znz_mul_c).
- Let w_mul         := w_op.(znz_mul).
- Let w_square_c    := w_op.(znz_square_c).
+ Let w_mul_c       := ZnZ.mul_c.
+ Let w_mul         := ZnZ.mul.
+ Let w_square_c    := ZnZ.square_c.
 
- Let w_div21       := w_op.(znz_div21).
- Let w_div_gt      := w_op.(znz_div_gt).
- Let w_div         := w_op.(znz_div).
+ Let w_div21       := ZnZ.div21.
+ Let w_div_gt      := ZnZ.div_gt.
+ Let w_div         := ZnZ.div.
 
- Let w_mod_gt      := w_op.(znz_mod_gt).
- Let w_mod         := w_op.(znz_mod).
+ Let w_mod_gt      := ZnZ.modulo_gt.
+ Let w_mod         := ZnZ.modulo.
 
- Let w_gcd_gt      := w_op.(znz_gcd_gt).
- Let w_gcd         := w_op.(znz_gcd).
+ Let w_gcd_gt      := ZnZ.gcd_gt.
+ Let w_gcd         := ZnZ.gcd.
 
- Let w_add_mul_div := w_op.(znz_add_mul_div).
+ Let w_add_mul_div := ZnZ.add_mul_div.
 
- Let w_pos_mod := w_op.(znz_pos_mod).
+ Let w_pos_mod := ZnZ.pos_mod.
 
- Let w_is_even     := w_op.(znz_is_even).
- Let w_sqrt2       := w_op.(znz_sqrt2).
- Let w_sqrt        := w_op.(znz_sqrt).
+ Let w_is_even     := ZnZ.is_even.
+ Let w_sqrt2       := ZnZ.sqrt2.
+ Let w_sqrt        := ZnZ.sqrt.
 
- Let _zn2z := zn2z w.
+ Let _zn2z := zn2z t.
 
  Let wB := base w_digits.
 
@@ -105,9 +103,9 @@ Section Z_2nZ.
 
  Let to_Z := zn2z_to_Z wB w_to_Z.
 
- Let w_W0 := znz_W0 w_op.
- Let w_0W := znz_0W w_op.
- Let w_WW := znz_WW w_op.
+ Let w_W0 := ZnZ.WO.
+ Let w_0W := ZnZ.OW.
+ Let w_WW := ZnZ.WW.
 
  Let ww_of_pos p :=
   match w_of_pos p with
@@ -124,15 +122,15 @@ Section Z_2nZ.
   Eval lazy beta delta [ww_tail0] in
   ww_tail0 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits.
 
- Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW w).
- Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W w).
- Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 w).
+ Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW t).
+ Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W t).
+ Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 t).
 
  (* ** Comparison ** *)
  Let compare :=
   Eval lazy beta delta[ww_compare] in ww_compare w_0 w_compare.
 
- Let eq0 (x:zn2z w) :=
+ Let eq0 (x:zn2z t) :=
   match x with
   | W0 => true
   | _ => false
@@ -226,7 +224,7 @@ Section Z_2nZ.
   Eval lazy beta iota delta [ww_div21] in
    ww_div21 w_0 w_0W div32 ww_1 compare sub.
 
- Let low (p: zn2z w) := match p with WW _ p1 => p1 | _ => w_0 end.
+ Let low (p: zn2z t) := match p with WW _ p1 => p1 | _ => w_0 end.
 
  Let add_mul_div :=
   Eval lazy beta delta [ww_add_mul_div] in
@@ -287,8 +285,8 @@ Section Z_2nZ.
 
  (* ** Record of operators on 2 words *)
 
- Definition mk_zn2z_op :=
-  mk_znz_op _ww_digits _ww_zdigits
+ Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 :=
+  ZnZ.MkOps _ww_digits _ww_zdigits
     to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
     compare eq0
@@ -307,8 +305,8 @@ Section Z_2nZ.
     sqrt2
     sqrt.
 
- Definition mk_zn2z_op_karatsuba :=
-   mk_znz_op _ww_digits _ww_zdigits
+ Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 :=
+   ZnZ.MkOps _ww_digits _ww_zdigits
     to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
     compare eq0
@@ -328,51 +326,51 @@ Section Z_2nZ.
     sqrt.
 
  (* Proof *)
- Variable op_spec : znz_spec w_op.
+ Context {specs : ZnZ.Specs ops}.
 
  Hint Resolve
-    (spec_to_Z op_spec)
-    (spec_of_pos op_spec)
-    (spec_0 op_spec)
-    (spec_1 op_spec)
-    (spec_Bm1 op_spec)
-    (spec_compare op_spec)
-    (spec_eq0 op_spec)
-    (spec_opp_c op_spec)
-    (spec_opp op_spec)
-    (spec_opp_carry op_spec)
-    (spec_succ_c op_spec)
-    (spec_add_c op_spec)
-    (spec_add_carry_c op_spec)
-    (spec_succ op_spec)
-    (spec_add op_spec)
-    (spec_add_carry op_spec)
-    (spec_pred_c op_spec)
-    (spec_sub_c op_spec)
-    (spec_sub_carry_c op_spec)
-    (spec_pred op_spec)
-    (spec_sub op_spec)
-    (spec_sub_carry op_spec)
-    (spec_mul_c op_spec)
-    (spec_mul op_spec)
-    (spec_square_c op_spec)
-    (spec_div21 op_spec)
-    (spec_div_gt op_spec)
-    (spec_div op_spec)
-    (spec_mod_gt op_spec)
-    (spec_mod op_spec)
-    (spec_gcd_gt op_spec)
-    (spec_gcd op_spec)
-    (spec_head0 op_spec)
-    (spec_tail0 op_spec)
-    (spec_add_mul_div op_spec)
-    (spec_pos_mod)
-    (spec_is_even)
-    (spec_sqrt2)
-    (spec_sqrt)
-    (spec_W0 op_spec)
-    (spec_0W op_spec)
-    (spec_WW op_spec).
+    ZnZ.spec_to_Z
+    ZnZ.spec_of_pos
+    ZnZ.spec_0
+    ZnZ.spec_1
+    ZnZ.spec_m1
+    ZnZ.spec_compare
+    ZnZ.spec_eq0
+    ZnZ.spec_opp_c
+    ZnZ.spec_opp
+    ZnZ.spec_opp_carry
+    ZnZ.spec_succ_c
+    ZnZ.spec_add_c
+    ZnZ.spec_add_carry_c
+    ZnZ.spec_succ
+    ZnZ.spec_add
+    ZnZ.spec_add_carry
+    ZnZ.spec_pred_c
+    ZnZ.spec_sub_c
+    ZnZ.spec_sub_carry_c
+    ZnZ.spec_pred
+    ZnZ.spec_sub
+    ZnZ.spec_sub_carry
+    ZnZ.spec_mul_c
+    ZnZ.spec_mul
+    ZnZ.spec_square_c
+    ZnZ.spec_div21
+    ZnZ.spec_div_gt
+    ZnZ.spec_div
+    ZnZ.spec_modulo_gt
+    ZnZ.spec_modulo
+    ZnZ.spec_gcd_gt
+    ZnZ.spec_gcd
+    ZnZ.spec_head0
+    ZnZ.spec_tail0
+    ZnZ.spec_add_mul_div
+    ZnZ.spec_pos_mod
+    ZnZ.spec_is_even
+    ZnZ.spec_sqrt2
+    ZnZ.spec_sqrt
+    ZnZ.spec_WO
+    ZnZ.spec_OW
+    ZnZ.spec_WW.
 
  Ltac wwauto := unfold ww_to_Z; auto.
 
@@ -395,16 +393,17 @@ Section Z_2nZ.
      Zpos p = (Z_of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|].
  Proof.
   unfold ww_of_pos;intros.
-  assert (H:= spec_of_pos op_spec p);unfold w_of_pos;
-   destruct (znz_of_pos w_op p). simpl in H.
-  rewrite H;clear H;destruct n;simpl to_Z.
-  simpl;unfold w_to_Z,w_0;rewrite (spec_0 op_spec);trivial.
-  unfold Z_of_N; assert (H:= spec_of_pos op_spec p0);
-  destruct (znz_of_pos w_op p0). simpl in H.
-  rewrite H;unfold fst, snd,Z_of_N, to_Z.
-  rewrite (spec_WW op_spec).
+  rewrite (ZnZ.spec_of_pos p). unfold w_of_pos.
+  case (ZnZ.of_pos p); intros. simpl.
+  destruct n; simpl ZnZ.to_Z.
+  simpl;unfold w_to_Z,w_0; rewrite ZnZ.spec_0;trivial.
+  unfold Z_of_N.
+  rewrite (ZnZ.spec_of_pos p0).
+  case (ZnZ.of_pos p0); intros. simpl.
+  unfold fst, snd,Z_of_N, to_Z, wB, w_digits, w_to_Z, w_WW.
+  rewrite ZnZ.spec_WW.
   replace wwB with (wB*wB).
-  unfold wB,w_to_Z,w_digits;clear H;destruct n;ring.
+  unfold wB,w_to_Z,w_digits;destruct n;ring.
   symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits).
  Qed.
 
@@ -418,15 +417,9 @@ Section Z_2nZ.
  Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
 
  Let spec_ww_compare :
-     forall x y,
-       match compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+  forall x y, compare x y = Zcompare [|x|] [|y|].
  Proof.
   refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto.
-  exact (spec_compare op_spec).
  Qed.
 
  Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0.
@@ -531,8 +524,7 @@ Section Z_2nZ.
  Proof.
  refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
           _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
-  unfold w_digits; apply spec_more_than_1_digit; auto.
-  exact (spec_compare op_spec).
+  unfold w_digits; apply ZnZ.spec_more_than_1_digit; auto.
  Qed.
 
  Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB.
@@ -559,11 +551,10 @@ Section Z_2nZ.
    w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z
    _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto.
   unfold w_Bm2, w_to_Z, w_pred, w_Bm1.
-  rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec).
+  rewrite ZnZ.spec_pred, ZnZ.spec_m1.
   unfold w_digits;rewrite Zmod_small. ring.
-  assert (H:= wB_pos(znz_digits w_op)). omega.
-  exact (spec_compare op_spec).
-  exact (spec_div21 op_spec).
+  assert (H:= wB_pos(ZnZ.digits)). omega.
+  exact ZnZ.spec_div21.
  Qed.
 
  Let spec_ww_div21 : forall a1 a2 b,
@@ -580,22 +571,19 @@ Section Z_2nZ.
  Let spec_add2: forall x y,
   [|w_add2 x y|] = w_to_Z x + w_to_Z y.
   unfold w_add2.
-  intros xh xl; generalize (spec_add_c op_spec xh xl).
-  unfold w_add_c; case znz_add_c; unfold interp_carry; simpl ww_to_Z.
+  intros xh xl; generalize (ZnZ.spec_add_c xh xl).
+  unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z.
     intros w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0.
-  unfold w_0; rewrite spec_0; simpl; auto with zarith.
+  unfold w_0; rewrite ZnZ.spec_0; simpl; auto with zarith.
   intros w0; rewrite Zmult_1_l; simpl.
-  unfold w_to_Z, w_1; rewrite spec_1; auto with zarith.
+  unfold w_to_Z, w_1; rewrite ZnZ.spec_1; auto with zarith.
   rewrite Zmult_1_l; auto.
  Qed.
 
  Let spec_low: forall x,
   w_to_Z (low x) = [|x|] mod wB.
   intros x; case x; simpl low.
-    unfold ww_to_Z, w_to_Z, w_0; rewrite (spec_0 op_spec); simpl.
-    rewrite Zmod_small; auto with zarith.
-    split; auto with zarith.
-    unfold wB, base; auto with zarith.
+    unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto.
   intros xh xl; simpl.
   rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith.
   rewrite Zmod_small; auto with zarith.
@@ -608,7 +596,7 @@ Section Z_2nZ.
  unfold w_to_Z, _ww_zdigits.
  rewrite spec_add2.
  unfold w_to_Z, w_zdigits, w_digits.
- rewrite spec_zdigits; auto.
+ rewrite ZnZ.spec_zdigits; auto.
  rewrite Zpos_xO; auto with zarith.
  Qed.
 
@@ -618,9 +606,8 @@ Section Z_2nZ.
  refine (spec_ww_head00 w_0 w_0W
                 w_compare w_head0 w_add2 w_zdigits _ww_zdigits
                 w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto.
- exact (spec_compare op_spec).
- exact (spec_head00 op_spec).
- exact (spec_zdigits op_spec).
+ exact ZnZ.spec_head00.
+ exact ZnZ.spec_zdigits.
  Qed.
 
  Let spec_ww_head0  : forall x,  0 < [|x|] ->
@@ -629,8 +616,7 @@ Section Z_2nZ.
   refine (spec_ww_head0 w_0 w_0W w_compare w_head0
            w_add2 w_zdigits _ww_zdigits
    w_to_Z _ _ _ _ _ _ _);wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
  Qed.
 
  Let spec_ww_tail00  : forall x,  [|x|] = 0 -> [|tail0 x|] = Zpos _ww_digits.
@@ -638,9 +624,8 @@ Section Z_2nZ.
  refine (spec_ww_tail00 w_0 w_0W
                 w_compare w_tail0 w_add2 w_zdigits _ww_zdigits
                 w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); wwauto.
- exact (spec_compare op_spec).
- exact (spec_tail00 op_spec).
- exact (spec_zdigits op_spec).
+ exact ZnZ.spec_tail00.
+ exact ZnZ.spec_zdigits.
  Qed.
 
 
@@ -649,8 +634,7 @@ Section Z_2nZ.
  Proof.
   refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0
            w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
  Qed.
 
  Lemma spec_ww_add_mul_div : forall x y p,
@@ -659,10 +643,10 @@ Section Z_2nZ.
          ([|x|] * (2 ^ [|p|]) +
           [|y|] / (2 ^ ((Zpos _ww_digits) - [|p|]))) mod wwB.
  Proof.
- refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W compare w_add_mul_div
+ refine (@spec_ww_add_mul_div t w_0 w_WW w_W0 w_0W compare w_add_mul_div
               sub w_digits w_zdigits low w_to_Z
            _ _ _ _ _ _ _ _ _ _ _);wwauto.
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
  Qed.
 
  Let spec_ww_div_gt : forall a b,
@@ -671,29 +655,29 @@ Section Z_2nZ.
       [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|].
  Proof.
 refine
-(@spec_ww_div_gt w w_digits w_0 w_WW w_0W w_compare w_eq0
+(@spec_ww_div_gt t w_digits w_0 w_WW w_0W w_compare w_eq0
    w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt
    w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
  _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
 ).
-  exact (spec_0 op_spec).
-  exact (spec_to_Z op_spec).
+  exact ZnZ.spec_0.
+  exact ZnZ.spec_to_Z.
   wwauto.
   wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_eq0 op_spec).
-  exact (spec_opp_c op_spec).
-  exact (spec_opp op_spec).
-  exact (spec_opp_carry op_spec).
-  exact (spec_sub_c op_spec).
-  exact (spec_sub op_spec).
-  exact (spec_sub_carry op_spec).
-  exact (spec_div_gt op_spec).
-  exact (spec_add_mul_div op_spec).
-  exact (spec_head0 op_spec).
-  exact (spec_div21 op_spec).
+  exact ZnZ.spec_compare.
+  exact ZnZ.spec_eq0.
+  exact ZnZ.spec_opp_c.
+  exact ZnZ.spec_opp.
+  exact ZnZ.spec_opp_carry.
+  exact ZnZ.spec_sub_c.
+  exact ZnZ.spec_sub.
+  exact ZnZ.spec_sub_carry.
+  exact ZnZ.spec_div_gt.
+  exact ZnZ.spec_add_mul_div.
+  exact ZnZ.spec_head0.
+  exact ZnZ.spec_div21.
   exact spec_w_div32.
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
   exact spec_ww_digits.
   exact spec_ww_1.
   exact spec_ww_add_mul_div.
@@ -711,15 +695,14 @@ refine
       [|a|] > [|b|] -> 0 < [|b|] ->
       [|mod_gt a b|] = [|a|] mod [|b|].
  Proof.
-  refine (@spec_ww_mod_gt w w_digits w_0 w_WW w_0W w_compare w_eq0
+  refine (@spec_ww_mod_gt t w_digits w_0 w_WW w_0W w_compare w_eq0
    w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt
    w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div
    w_zdigits w_to_Z
    _ _ _ _ _   _ _ _ _ _   _ _ _ _ _   _ _ _ _ _ _ _);wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_div_gt op_spec).
-  exact (spec_div21 op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_div_gt.
+  exact ZnZ.spec_div21.
+  exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
  Qed.
 
@@ -731,37 +714,33 @@ refine
  Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] ->
       Zis_gcd [|a|] [|b|] [|gcd_gt a b|].
  Proof.
-  refine (@spec_ww_gcd_gt w w_digits W0 w_to_Z _
+  refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _
     w_0 w_0 w_eq0 w_gcd_gt _ww_digits
   _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
-  refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
+  refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
    _ _ _ _ _   _ _ _ _ _   _ _ _ _ _   _ _ _ _ _);wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_div21 op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_div21.
+  exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
-  refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
+  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
    _ _);auto.
- exact (spec_compare op_spec).
  Qed.
 
  Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
  Proof.
-  refine (@spec_ww_gcd w w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
+  refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
   _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
-  refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
+  refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
    _ _ _ _ _   _ _ _ _ _   _ _ _ _ _   _ _ _ _ _);wwauto.
-  exact (spec_compare op_spec).
-  exact (spec_div21 op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_div21.
+  exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
-  refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
+  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
    _ _);auto.
-  exact (spec_compare op_spec).
  Qed.
 
  Let spec_ww_is_even : forall x,
@@ -770,8 +749,8 @@ refine
       | false => [|x|] mod 2 = 1
       end.
  Proof.
- refine (@spec_ww_is_even w w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto.
- exact (spec_is_even op_spec).
+ refine (@spec_ww_is_even t w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto.
+ exact ZnZ.spec_is_even.
  Qed.
 
  Let spec_ww_sqrt2 : forall x y,
@@ -781,60 +760,57 @@ refine
           [+|r|] <= 2 * [|s|].
  Proof.
  intros x y H.
- refine (@spec_ww_sqrt2 w w_is_even w_compare w_0 w_1 w_Bm1
+ refine (@spec_ww_sqrt2 t w_is_even w_compare w_0 w_1 w_Bm1
                w_0W w_sub w_square_c w_div21 w_add_mul_div w_digits w_zdigits
                _ww_zdigits
                w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div
                 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
- exact (spec_zdigits op_spec).
- exact (spec_more_than_1_digit op_spec).
- exact (spec_is_even op_spec).
- exact (spec_compare op_spec).
- exact (spec_div21 op_spec).
- exact (spec_ww_add_mul_div).
- exact (spec_sqrt2 op_spec).
+ exact ZnZ.spec_zdigits.
+ exact ZnZ.spec_more_than_1_digit.
+ exact ZnZ.spec_is_even.
+ exact ZnZ.spec_div21.
+ exact spec_ww_add_mul_div.
+ exact ZnZ.spec_sqrt2.
  Qed.
 
  Let spec_ww_sqrt : forall x,
        [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.
  Proof.
- refine (@spec_ww_sqrt w w_is_even w_0 w_1 w_Bm1
+ refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1
            w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits
                w_sqrt2 pred add_mul_div head0 compare
             _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
- exact (spec_zdigits op_spec).
- exact (spec_more_than_1_digit op_spec).
- exact (spec_is_even op_spec).
- exact (spec_ww_add_mul_div).
- exact (spec_sqrt2 op_spec).
+ exact ZnZ.spec_zdigits.
+ exact ZnZ.spec_more_than_1_digit.
+ exact ZnZ.spec_is_even.
+ exact spec_ww_add_mul_div.
+ exact ZnZ.spec_sqrt2.
  Qed.
 
- Lemma mk_znz2_spec : znz_spec mk_zn2z_op.
+ Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops.
  Proof.
-  apply mk_znz_spec;auto.
+  apply ZnZ.MkSpecs; auto.
   exact spec_ww_add_mul_div.
 
-  refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW
+  refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW
            w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z
        _ _ _ _ _ _ _ _ _ _ _ _);wwauto.
-  exact (spec_pos_mod op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
   unfold w_to_Z, w_zdigits.
-  rewrite (spec_zdigits op_spec).
+  rewrite ZnZ.spec_zdigits.
   rewrite <- Zpos_xO; exact spec_ww_digits.
  Qed.
 
- Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba.
+ Global Instance mk_zn2z_specs_karatsuba : ZnZ.Specs mk_zn2z_ops_karatsuba.
  Proof.
-  apply mk_znz_spec;auto.
+  apply ZnZ.MkSpecs; auto.
   exact spec_ww_add_mul_div.
-  refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW
+  refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW
            w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z
        _ _ _ _ _ _ _ _ _ _ _ _);wwauto.
-  exact (spec_pos_mod op_spec).
-  exact (spec_zdigits op_spec).
+  exact ZnZ.spec_zdigits.
   unfold w_to_Z, w_zdigits.
-  rewrite (spec_zdigits op_spec).
+  rewrite ZnZ.spec_zdigits.
   rewrite <- Zpos_xO; exact spec_ww_digits.
  Qed.
 
@@ -842,17 +818,14 @@ End Z_2nZ.
 
 Section MulAdd.
 
-  Variable w: Type.
-  Variable op: znz_op w.
-  Variable sop: znz_spec op.
+  Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}.
 
-  Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op).
+  Definition mul_add:= w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c.
 
-  Notation "[| x |]" := (znz_to_Z op x)  (at level 0, x at level 99).
+  Notation "[| x |]" := (ZnZ.to_Z x)  (at level 0, x at level 99).
 
   Notation "[|| x ||]" :=
-   (zn2z_to_Z (base (znz_digits op)) (znz_to_Z op) x)  (at level 0, x at level 99).
-
+   (zn2z_to_Z (base ZnZ.digits) ZnZ.to_Z x)  (at level 0, x at level 99).
 
   Lemma spec_mul_add: forall x y z,
      let (zh, zl) := mul_add x y z in
@@ -860,11 +833,11 @@ Section MulAdd.
   Proof.
   intros x y z.
    refine (spec_w_mul_add _ _ _ _ _ _ _ _ _ _ _ _ x y z); auto.
-  exact (spec_0 sop).
-  exact (spec_to_Z sop).
-  exact (spec_succ sop).
-  exact (spec_add_c sop).
-  exact (spec_mul_c sop).
+  exact ZnZ.spec_0.
+  exact ZnZ.spec_to_Z.
+  exact ZnZ.spec_succ.
+  exact ZnZ.spec_add_c.
+  exact ZnZ.spec_mul_c.
   Qed.
 
 End MulAdd.
@@ -873,13 +846,13 @@ End MulAdd.
 (** Modular versions of DoubleCyclic *)
 
 Module DoubleCyclic (C:CyclicType) <: CyclicType.
- Definition w := zn2z C.w.
- Definition w_op := mk_zn2z_op C.w_op.
- Definition w_spec := mk_znz2_spec C.w_spec.
+ Definition t := zn2z C.t.
+ Instance ops : ZnZ.Ops t := mk_zn2z_ops.
+ Instance specs : ZnZ.Specs ops := mk_zn2z_specs.
 End DoubleCyclic.
 
 Module DoubleCyclicKaratsuba (C:CyclicType) <: CyclicType.
- Definition w := zn2z C.w.
- Definition w_op := mk_zn2z_op_karatsuba C.w_op.
- Definition w_spec := mk_znz2_karatsuba_spec C.w_spec.
+ Definition t := zn2z C.t.
+ Definition ops : ZnZ.Ops t := mk_zn2z_ops_karatsuba.
+ Definition specs : ZnZ.Specs ops := mk_zn2z_specs_karatsuba.
 End DoubleCyclicKaratsuba.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 4e6eccea..0cb6848e 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*         Benjamin Gregoire, Laurent Thery, INRIA, 2007                *)
 (************************************************************************)
 
-(*i $Id: DoubleDiv.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -82,11 +80,7 @@ Section POS_MOD.
 
   Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
   Variable spec_ww_compare : forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+    ww_compare x y = Zcompare [[x]] [[y]].
  Variable spec_ww_sub: forall x y,
    [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
 
@@ -105,8 +99,8 @@ Section POS_MOD.
  intros w1 p; case (spec_to_w_Z p); intros HH1 HH2.
  unfold ww_pos_mod; case w1.
  simpl; rewrite Zmod_small; split; auto with zarith.
- intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits));
-    case ww_compare;
+ intros xh xl; rewrite spec_ww_compare.
+    case Zcompare_spec;
     rewrite spec_w_0W; rewrite spec_zdigits; fold wB;
     intros H1.
    rewrite H1; simpl ww_to_Z.
@@ -134,8 +128,8 @@ Section POS_MOD.
    rewrite Z_mod_mult; auto with zarith.
    autorewrite with w_rewrite rm10.
    rewrite Zmod_mod; auto with zarith.
-generalize (spec_ww_compare p ww_zdigits);
-    case ww_compare; rewrite spec_ww_zdigits;
+  rewrite spec_ww_compare.
+    case Zcompare_spec; rewrite spec_ww_zdigits;
                      rewrite spec_zdigits; intros H2.
   replace (2^[[p]]) with wwB.
     rewrite Zmod_small; auto with zarith.
@@ -266,12 +260,7 @@ Section DoubleDiv32.
 
   Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
   Variable spec_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+     forall x y, w_compare x y = Zcompare [|x|] [|y|].
   Variable spec_w_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
   Variable spec_w_add_carry_c :
          forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1.
@@ -343,7 +332,7 @@ Section DoubleDiv32.
      (WW (w_sub a2 b2) a3) (WW b1 b2)
     | Gt => (w_0, W0) (* cas absurde *)
     end.
-   assert (Hcmp:=spec_compare a1 b1);destruct (w_compare a1 b1).
+   rewrite spec_compare. case Zcompare_spec; intro Hcmp.
    simpl in Hlt.
    rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega.
    assert ([[WW (w_sub a2 b2) a3]] = ([|a2|]-[|b2|])*wB + [|a3|] + wwB).
@@ -545,11 +534,7 @@ Section DoubleDiv21.
      0 <= [[r]] < [|b1|] * wB + [|b2|].
   Variable spec_ww_1 : [[ww_1]] = 1.
   Variable spec_ww_compare :  forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+    ww_compare x y = Zcompare [[x]] [[y]].
   Variable spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
 
   Theorem wwB_div: wwB  = 2 * (wwB / 2).
@@ -576,10 +561,9 @@ Section DoubleDiv21.
    intros a1 a2 b H Hlt; unfold ww_div21.
    Spec_ww_to_Z b; assert (Eq: 0 < [[b]]).    Spec_ww_to_Z a1;omega.
    generalize Hlt H ;clear Hlt H;case a1.
-   intros H1 H2;simpl in H1;Spec_ww_to_Z a2;
-   match goal with |-context [ww_compare ?Y ?Z] =>
-     generalize (spec_ww_compare Y Z); case (ww_compare Y Z)
-   end; simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith.
+   intros H1 H2;simpl in H1;Spec_ww_to_Z a2.
+   rewrite spec_ww_compare. case Zcompare_spec;
+   simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith.
    rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith.
    split. ring.
    assert (wwB <= 2*[[b]]);zarith.
@@ -809,12 +793,7 @@ Section DoubleDivGt.
   Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
   Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
   Variable spec_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+     forall x y, w_compare x y = Zcompare [|x|] [|y|].
   Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
 
   Variable spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|].
@@ -914,7 +893,7 @@ Section DoubleDivGt.
     end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]).
    assert (Hh := spec_head0 Hpos).
    lazy zeta.
-   generalize (spec_compare (w_head0 bh) w_0); case w_compare;
+   rewrite spec_compare; case Zcompare_spec;
     rewrite spec_w_0; intros HH.
    generalize Hh; rewrite HH; simpl Zpower;
         rewrite Zmult_1_l; intros (HH1, HH2); clear HH.
@@ -1058,14 +1037,13 @@ Section DoubleDivGt.
    assert (H2:=spec_div_gt Hgt Hpos);destruct (w_div_gt al bl).
    repeat rewrite spec_w_0W;simpl;rewrite spec_w_0;simpl;trivial.
    clear H.
-   assert (Hcmp := spec_compare w_0 bh); destruct (w_compare w_0 bh).
+   rewrite spec_compare; case Zcompare_spec; intros Hcmp.
    rewrite spec_w_0 in Hcmp. change [[WW bh bl]] with ([|bh|]*wB+[|bl|]).
    rewrite <- Hcmp;rewrite Zmult_0_l;rewrite Zplus_0_l.
    simpl in Hpos;rewrite <- Hcmp in Hpos;simpl in Hpos.
    assert (H2:= @spec_double_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
     w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0
     spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos).
-   unfold double_to_Z,double_wB,double_digits in H2.
    destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
               w_compare w_sub 1
              (WW ah al) bl).
@@ -1154,7 +1132,7 @@ Section DoubleDivGt.
    rewrite spec_w_0W;rewrite spec_w_mod_gt_eq;trivial.
    destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial.
    clear H.
-   assert (H2 := spec_compare w_0 bh);destruct (w_compare w_0 bh).
+   rewrite spec_compare; case Zcompare_spec; intros H2.
    rewrite (@spec_double_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div
             w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl).
    destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1
@@ -1227,13 +1205,14 @@ Section DoubleDivGt.
       end
     | Gt => W0 (* absurde *)
     end).
-   assert (Hbh := spec_compare w_0 bh);destruct (w_compare w_0 bh).
-   simpl ww_to_Z in *. rewrite spec_w_0 in Hbh;rewrite <- Hbh;
+   rewrite spec_compare, spec_w_0.
+   case Zcompare_spec; intros Hbh.
+   simpl ww_to_Z in *. rewrite <- Hbh.
    rewrite Zmult_0_l;rewrite Zplus_0_l.
-   assert (Hbl := spec_compare w_0 bl); destruct (w_compare w_0 bl).
-   rewrite spec_w_0 in Hbl;rewrite <- Hbl;apply Zis_gcd_0.
+   rewrite spec_compare, spec_w_0.
+   case Zcompare_spec; intros Hbl.
+   rewrite <- Hbl;apply Zis_gcd_0.
    simpl;rewrite spec_w_0;rewrite Zmult_0_l;rewrite Zplus_0_l.
-   rewrite spec_w_0 in Hbl.
    apply Zis_gcd_mod;zarith.
    change ([|ah|] * wB + [|al|]) with (double_to_Z w_digits w_to_Z 1 (WW ah al)).
    rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
@@ -1243,20 +1222,20 @@ Section DoubleDivGt.
    rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
    apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
     destruct (Z_mod_lt x y);zarith end.
-   rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;exfalso;omega.
-   rewrite spec_w_0 in Hbh;assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh).
+   Spec_w_to_Z bl;exfalso;omega.
+   assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh).
    assert (H2 : 0 < [[WW bh bl]]).
    simpl;Spec_w_to_Z bl. apply Zlt_le_trans with ([|bh|]*wB);zarith.
    apply Zmult_lt_0_compat;zarith.
    apply Zis_gcd_mod;trivial. rewrite <- H.
    simpl in *;destruct (ww_mod_gt_aux ah al bh bl) as [ |mh ml].
    simpl;apply Zis_gcd_0;zarith.
-   assert (Hmh := spec_compare w_0 mh);destruct (w_compare w_0 mh).
-   simpl;rewrite spec_w_0 in Hmh; rewrite <- Hmh;simpl.
-   assert (Hml := spec_compare w_0 ml);destruct (w_compare w_0 ml).
-   rewrite <- Hml;rewrite spec_w_0;simpl;apply Zis_gcd_0.
-   simpl;rewrite spec_w_0;simpl.
-   rewrite spec_w_0 in Hml. apply Zis_gcd_mod;zarith.
+   rewrite spec_compare, spec_w_0; case Zcompare_spec; intros Hmh.
+   simpl;rewrite <- Hmh;simpl.
+   rewrite spec_compare, spec_w_0; case Zcompare_spec; intros Hml.
+   rewrite <- Hml;simpl;apply Zis_gcd_0.
+   simpl; rewrite spec_w_0; simpl.
+   apply Zis_gcd_mod;zarith.
    change ([|bh|] * wB + [|bl|]) with (double_to_Z w_digits w_to_Z 1 (WW bh bl)).
    rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
    w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div
@@ -1265,8 +1244,8 @@ Section DoubleDivGt.
    rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
    apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
    destruct (Z_mod_lt x y);zarith end.
-   rewrite spec_w_0 in Hml;Spec_w_to_Z ml;exfalso;omega.
-   rewrite spec_w_0 in Hmh. assert ([[WW bh bl]] > [[WW mh ml]]).
+   Spec_w_to_Z ml;exfalso;omega.
+   assert ([[WW bh bl]] > [[WW mh ml]]).
    rewrite H;simpl; apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
    destruct (Z_mod_lt x y);zarith end.
    assert (H1:= spec_ww_mod_gt_aux _ _ _ H0 Hmh).
@@ -1300,8 +1279,8 @@ Section DoubleDivGt.
    rewrite Z_div_mult;zarith.
    assert (2^1 <= 2^n). change (2^1) with 2;zarith.
    assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith.
-   rewrite spec_w_0 in Hmh;Spec_w_to_Z mh;exfalso;zarith.
-   rewrite spec_w_0 in Hbh;Spec_w_to_Z bh;exfalso;zarith.
+   Spec_w_to_Z mh;exfalso;zarith.
+   Spec_w_to_Z bh;exfalso;zarith.
   Qed.
 
   Lemma spec_ww_gcd_gt_aux :
@@ -1374,11 +1353,7 @@ Section DoubleDiv.
   Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
   Variable spec_ww_1 : [[ww_1]] = 1.
   Variable spec_ww_compare :  forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+    ww_compare x y = Zcompare [[x]] [[y]].
   Variable spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
       let (q,r) := ww_div_gt a b in
       [[a]] = [[q]] * [[b]] + [[r]] /\
@@ -1400,20 +1375,20 @@ Section DoubleDiv.
       0 <= [[r]] < [[b]].
   Proof.
    intros a b Hpos;unfold ww_div.
-   assert (H:=spec_ww_compare a b);destruct (ww_compare a b).
+   rewrite spec_ww_compare; case Zcompare_spec; intros.
    simpl;rewrite spec_ww_1;split;zarith.
    simpl;split;[ring|Spec_ww_to_Z a;zarith].
-   apply spec_ww_div_gt;trivial.
+   apply spec_ww_div_gt;auto with zarith.
   Qed.
 
   Lemma  spec_ww_mod :  forall a b, 0 < [[b]] ->
       [[ww_mod a b]] = [[a]] mod [[b]].
   Proof.
    intros a b Hpos;unfold ww_mod.
-   assert (H := spec_ww_compare a b);destruct (ww_compare a b).
+   rewrite spec_ww_compare; case Zcompare_spec; intros.
    simpl;apply Zmod_unique with 1;try rewrite H;zarith.
    Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith.
-   apply spec_ww_mod_gt;trivial.
+   apply spec_ww_mod_gt;auto with zarith.
   Qed.
 
 
@@ -1431,12 +1406,7 @@ Section DoubleDiv.
   Variable spec_w_0   : [|w_0|] = 0.
   Variable spec_w_1   : [|w_1|] = 1.
   Variable spec_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+    forall x y, w_compare x y = Zcompare [|x|] [|y|].
   Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
   Variable spec_gcd_gt : forall a b, [|a|] > [|b|] ->
       Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|].
@@ -1468,14 +1438,14 @@ Section DoubleDiv.
     assert (0 <= 1 < wB). split;zarith. apply wB_pos.
     assert (H1:= beta_lex _ _ _ _ _ Hle (spec_to_Z yl) H).
     Spec_w_to_Z yh;zarith.
-   unfold gcd_cont;assert (Hcmpy:=spec_compare w_1 yl);
-   rewrite spec_w_1 in Hcmpy.
-   simpl;rewrite H;simpl;destruct (w_compare w_1 yl).
+   unfold gcd_cont; rewrite spec_compare, spec_w_1.
+   case Zcompare_spec; intros Hcmpy.
+   simpl;rewrite H;simpl;
    rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod;zarith.
    rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith.
    rewrite H in Hle; exfalso;zarith.
-   assert ([|yl|] = 0). Spec_w_to_Z yl;zarith.
-   rewrite H0;simpl;apply Zis_gcd_0;trivial.
+   assert (H0 : [|yl|] = 0) by (Spec_w_to_Z yl;zarith).
+   simpl. rewrite H0, H;simpl;apply Zis_gcd_0;trivial.
   Qed.
 
 
@@ -1528,7 +1498,7 @@ Section DoubleDiv.
      | Eq => a
      | Lt => ww_gcd_gt b a
      end).
-   assert (Hcmp := spec_ww_compare a b);destruct (ww_compare a b).
+   rewrite spec_ww_compare; case Zcompare_spec; intros Hcmp.
    Spec_ww_to_Z b;rewrite Hcmp.
    apply Zis_gcd_for_euclid with 1;zarith.
    ring_simplify ([[b]] - 1 * [[b]]). apply Zis_gcd_0;zarith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 4bdb75d6..062282f2 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,17 +8,17 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleDivn1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
 
+Local Infix "<<" := Pos.shiftl_nat (at level 30).
+
 Section GENDIVN1.
 
  Variable w             : Type.
@@ -62,12 +62,7 @@ Section GENDIVN1.
      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].
  Variable spec_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+   forall x y, w_compare x y = Zcompare [|x|] [|y|].
  Variable spec_sub: forall x y,
    [|w_sub x y|] = ([|x|] - [|y|]) mod wB.
 
@@ -162,14 +157,10 @@ Section GENDIVN1.
    | S n => double_divn1_p_aux n (double_divn1_p n)
    end.
 
-  Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n).
+  Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).
   Proof.
-(*
-   induction n;simpl. destruct p_bounded;trivial.
-   case (spec_to_Z p); rewrite Zpos_xO;auto with zarith.
-*)
    induction n;simpl. trivial.
-   case (spec_to_Z p); rewrite Zpos_xO;auto with zarith.
+   case (spec_to_Z p); rewrite Pshiftl_nat_S, Zpos_xO;auto with zarith.
   Qed.
 
   Lemma spec_double_divn1_p : forall n r h l,
@@ -177,14 +168,14 @@ Section GENDIVN1.
     let (q,r') := double_divn1_p n r h l in
     [|r|] * double_wB w_digits n +
       ([!n|h!]*2^[|p|] +
-        [!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|])))
+        [!n|l!] / (2^(Zpos(w_digits << n) - [|p|])))
         mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\
     0 <= [|r'|] < [|b2p|].
   Proof.
    case (spec_to_Z p); intros HH0 HH1.
    induction n;intros.
    simpl (double_divn1_p 0 r h l).
-   unfold double_to_Z, double_wB, double_digits.
+   unfold double_to_Z, double_wB, "<<".
    rewrite <- spec_add_mul_divp.
    exact (spec_div21 (w_add_mul_div p h l) b2p_le H).
    simpl (double_divn1_p (S n) r h l).
@@ -196,24 +187,24 @@ Section GENDIVN1.
    replace ([|r|] * (double_wB w_digits n * double_wB w_digits n) +
     (([!n|hh!] * double_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] +
     ([!n|lh!] * double_wB w_digits n + [!n|ll!]) /
-     2^(Zpos (double_digits w_digits (S n)) - [|p|])) mod
+     2^(Zpos (w_digits << (S n)) - [|p|])) mod
       (double_wB w_digits n * double_wB w_digits n)) with
     (([|r|] * double_wB w_digits n + ([!n|hh!] * 2^[|p|] +
-      [!n|hl!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|hl!] / 2^(Zpos (w_digits << n) - [|p|])) mod
                       double_wB w_digits n) * double_wB w_digits n +
      ([!n|hl!] * 2^[|p|] +
-      [!n|lh!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|lh!] / 2^(Zpos (w_digits << n) - [|p|])) mod
               double_wB w_digits n).
    generalize (IHn r hh hl H);destruct (double_divn1_p n r hh hl) as (qh,rh);
    intros (H3,H4);rewrite H3.
    assert ([|rh|] < [|b2p|]). omega.
    replace (([!n|qh!] * [|b2p|] + [|rh|]) * double_wB w_digits n +
      ([!n|hl!] * 2 ^ [|p|] +
-      [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod
       double_wB w_digits n)  with
     ([!n|qh!] * [|b2p|] *double_wB w_digits n + ([|rh|]*double_wB w_digits n +
       ([!n|hl!] * 2 ^ [|p|] +
-       [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod
+       [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod
       double_wB w_digits n)). 2:ring.
    generalize (IHn rh hl lh H0);destruct (double_divn1_p n rh hl lh) as (ql,rl);
    intros (H5,H6);rewrite H5.
@@ -229,52 +220,52 @@ Section GENDIVN1.
    unfold double_wB,base.
    assert (UU:=p_lt_double_digits n).
    rewrite Zdiv_shift_r;auto with zarith.
-   2:change (Zpos (double_digits w_digits (S n)))
-     with (2*Zpos (double_digits w_digits n));auto with zarith.
-   replace (2 ^ (Zpos (double_digits w_digits (S n)) - [|p|])) with
-    (2^(Zpos (double_digits w_digits n) - [|p|])*2^Zpos (double_digits w_digits n)).
+   2:change (Zpos (w_digits << (S n)))
+     with (2*Zpos (w_digits << n));auto with zarith.
+   replace (2 ^ (Zpos (w_digits << (S n)) - [|p|])) with
+    (2^(Zpos (w_digits << n) - [|p|])*2^Zpos (w_digits << n)).
    rewrite Zdiv_mult_cancel_r;auto with zarith.
    rewrite Zmult_plus_distr_l with (p:=  2^[|p|]).
    pattern  ([!n|hl!] * 2^[|p|]) at 2;
-   rewrite (shift_unshift_mod (Zpos(double_digits w_digits n))([|p|])([!n|hl!]));
+   rewrite (shift_unshift_mod (Zpos(w_digits << n))([|p|])([!n|hl!]));
     auto with zarith.
    rewrite Zplus_assoc.
    replace
-    ([!n|hh!] * 2^Zpos (double_digits w_digits n)* 2^[|p|] +
-      ([!n|hl!] / 2^(Zpos (double_digits w_digits n)-[|p|])*
-       2^Zpos(double_digits w_digits n)))
+    ([!n|hh!] * 2^Zpos (w_digits << n)* 2^[|p|] +
+      ([!n|hl!] / 2^(Zpos (w_digits << n)-[|p|])*
+       2^Zpos(w_digits << n)))
    with
     (([!n|hh!] *2^[|p|] + double_to_Z w_digits w_to_Z n hl /
-       2^(Zpos (double_digits w_digits n)-[|p|]))
-      * 2^Zpos(double_digits w_digits n));try (ring;fail).
+       2^(Zpos (w_digits << n)-[|p|]))
+      * 2^Zpos(w_digits << n));try (ring;fail).
    rewrite <- Zplus_assoc.
    rewrite <- (Zmod_shift_r ([|p|]));auto with zarith.
    replace
-     (2 ^ Zpos (double_digits w_digits n) * 2 ^ Zpos (double_digits w_digits n)) with
-     (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))).
-   rewrite (Zmod_shift_r (Zpos (double_digits w_digits n)));auto with zarith.
-   replace (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n)))
-   with (2^Zpos(double_digits w_digits n) *2^Zpos(double_digits w_digits n)).
+     (2 ^ Zpos (w_digits << n) * 2 ^ Zpos (w_digits << n)) with
+     (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))).
+   rewrite (Zmod_shift_r (Zpos (w_digits << n)));auto with zarith.
+   replace (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n)))
+   with (2^Zpos(w_digits << n) *2^Zpos(w_digits << n)).
    rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] +
-      [!n|hl!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])))).
+      [!n|hl!] / 2 ^ (Zpos (w_digits << n) - [|p|])))).
    rewrite  Zmult_mod_distr_l;auto with zarith.
    ring.
    rewrite Zpower_exp;auto with zarith.
-   assert (0 < Zpos (double_digits w_digits n)). unfold Zlt;reflexivity.
+   assert (0 < Zpos (w_digits << n)). unfold Zlt;reflexivity.
    auto with zarith.
    apply Z_mod_lt;auto with zarith.
    rewrite Zpower_exp;auto with zarith.
    split;auto with zarith.
    apply Zdiv_lt_upper_bound;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace ([|p|] + (Zpos (double_digits w_digits n) - [|p|])) with
-     (Zpos(double_digits w_digits n));auto with zarith.
+   replace ([|p|] + (Zpos (w_digits << n) - [|p|])) with
+     (Zpos(w_digits << n));auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace (Zpos (double_digits w_digits (S n)) - [|p|]) with
-       (Zpos (double_digits w_digits n) - [|p|] +
-         Zpos (double_digits w_digits n));trivial.
-   change (Zpos (double_digits w_digits (S n))) with
-    (2*Zpos (double_digits w_digits n)). ring.
+   replace (Zpos (w_digits << (S n)) - [|p|]) with
+       (Zpos (w_digits << n) - [|p|] +
+         Zpos (w_digits << n));trivial.
+   change (Zpos (w_digits << (S n))) with
+    (2*Zpos (w_digits << n)). ring.
   Qed.
 
   Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:=
@@ -311,20 +302,21 @@ Section GENDIVN1.
      end
   end.
 
- Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n).
+ Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n).
  Proof.
   induction n;simpl;auto with zarith.
-  change (Zpos (xO (double_digits w_digits n))) with
-    (2*Zpos (double_digits w_digits n)).
-  assert (0 < Zpos w_digits);auto with zarith.
-  exact (refl_equal Lt).
+  rewrite Pshiftl_nat_S.
+  change (Zpos (xO (w_digits << n))) with
+    (2*Zpos (w_digits << n)).
+  assert (0 < Zpos w_digits) by reflexivity.
+  auto with zarith.
  Qed.
 
  Lemma spec_high : forall n (x:word w n),
-   [|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits).
+   [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits).
  Proof.
   induction n;intros.
-  unfold high,double_digits,double_to_Z.
+  unfold high,double_to_Z. rewrite Pshiftl_nat_0.
   replace (Zpos w_digits - Zpos w_digits) with 0;try ring.
   simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith.
   assert (U2 := spec_double_digits n).
@@ -336,18 +328,18 @@ Section GENDIVN1.
    assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1).
   simpl [!S n|WW w0 w1!].
   unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith.
-  replace (2 ^ (Zpos (double_digits w_digits (S n)) - Zpos w_digits)) with
-   (2^(Zpos (double_digits w_digits n) - Zpos w_digits) *
-        2^Zpos (double_digits w_digits n)).
+  replace (2 ^ (Zpos (w_digits << (S n)) - Zpos w_digits)) with
+   (2^(Zpos (w_digits << n) - Zpos w_digits) *
+        2^Zpos (w_digits << n)).
   rewrite Zdiv_mult_cancel_r;auto with zarith.
   rewrite <- Zpower_exp;auto with zarith.
-  replace (Zpos (double_digits w_digits n) - Zpos w_digits +
-    Zpos (double_digits w_digits n)) with
-   (Zpos (double_digits w_digits (S n)) - Zpos w_digits);trivial.
-  change (Zpos (double_digits w_digits (S n))) with
-     (2*Zpos (double_digits w_digits n));ring.
-  change (Zpos (double_digits w_digits (S n))) with
-  (2*Zpos (double_digits w_digits n)); auto with zarith.
+  replace (Zpos (w_digits << n) - Zpos w_digits +
+    Zpos (w_digits << n)) with
+   (Zpos (w_digits << (S n)) - Zpos w_digits);trivial.
+  change (Zpos (w_digits << (S n))) with
+     (2*Zpos (w_digits << n));ring.
+  change (Zpos (w_digits << (S n))) with
+  (2*Zpos (w_digits << n)); auto with zarith.
  Qed.
 
  Definition double_divn1 (n:nat) (a:word w n) (b:w) :=
@@ -373,7 +365,7 @@ Section GENDIVN1.
    intros n a b H. unfold double_divn1.
    case (spec_head0 H); intros H0 H1.
    case (spec_to_Z (w_head0 b)); intros HH1 HH2.
-   generalize (spec_compare (w_head0 b) w_0); case w_compare;
+   rewrite spec_compare; case Zcompare_spec;
      rewrite spec_0; intros H2; auto with zarith.
    assert (Hv1: wB/2 <= [|b|]).
      generalize H0; rewrite H2; rewrite Zpower_0_r;
@@ -432,13 +424,13 @@ Section GENDIVN1.
    rewrite spec_add_mul_div in H7;auto with zarith.
    rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7.
    assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB
-     = [!n|a!] / 2^(Zpos (double_digits w_digits n) - [|w_head0 b|])).
+     = [!n|a!] / 2^(Zpos (w_digits << n) - [|w_head0 b|])).
    rewrite Zmod_small;auto with zarith.
    rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace (Zpos (double_digits w_digits n) - Zpos w_digits +
+   replace (Zpos (w_digits << n) - Zpos w_digits +
                        (Zpos w_digits - [|w_head0 b|]))
-    with (Zpos (double_digits w_digits n) - [|w_head0 b|]);trivial;ring.
+    with (Zpos (w_digits << n) - [|w_head0 b|]);trivial;ring.
    assert (H8 := Zpower_gt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
    split;auto with zarith.
    apply Zle_lt_trans with ([|high n a|]);auto with zarith.
@@ -506,7 +498,7 @@ Section GENDIVN1.
     double_modn1 n a b = snd (double_divn1 n a b).
  Proof.
   intros n a b;unfold double_divn1,double_modn1.
-  generalize (spec_compare (w_head0 b) w_0); case w_compare;
+  rewrite spec_compare; case Zcompare_spec;
      rewrite spec_0; intros H2; auto with zarith.
   apply spec_double_modn1_0.
   apply spec_double_modn1_0.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 36e3da9b..a6a0fc8e 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleLift.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -106,17 +104,9 @@ Section DoubleLift.
   Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
   Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
   Variable spec_compare : forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+   w_compare x y = Zcompare [|x|] [|y|].
   Variable spec_ww_compare : forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+   ww_compare x y = Zcompare [[x]] [[y]].
   Variable spec_ww_digits : ww_Digits = xO w_digits.
   Variable spec_w_head00  : forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits.
   Variable spec_w_head0  : forall x,  0 < [|x|] ->
@@ -159,7 +149,7 @@ Section DoubleLift.
     absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
     rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith.
     apply Zmult_lt_0_compat; auto with zarith.
-  generalize (spec_compare w_0 xh); case w_compare.
+  rewrite spec_compare. case Zcompare_spec.
     intros H; simpl.
     rewrite spec_w_add; rewrite spec_w_head00.
     rewrite spec_zdigits; rewrite spec_ww_digits.
@@ -176,9 +166,8 @@ Section DoubleLift.
    rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB.
    assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H.
    unfold Zlt in H;discriminate H.
-   assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0.
-   destruct (w_compare w_0 xh).
-   rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H.
+   rewrite spec_compare, spec_w_0. case Zcompare_spec; intros H0.
+   rewrite <- H0 in *. simpl Zplus. simpl in H.
    case (spec_to_Z w_zdigits);
      case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4.
    rewrite spec_w_add.
@@ -233,7 +222,7 @@ Section DoubleLift.
     apply Zmult_lt_0_compat; auto with zarith.
   assert (F2: [|xl|] = 0).
     rewrite F1 in Hx; auto with zarith.
-  generalize (spec_compare w_0 xl); case w_compare.
+  rewrite spec_compare; case Zcompare_spec.
     intros H; simpl.
     rewrite spec_w_add; rewrite spec_w_tail00; auto.
     rewrite spec_zdigits; rewrite spec_ww_digits.
@@ -248,8 +237,7 @@ Section DoubleLift.
    clear spec_ww_zdigits.
    destruct x as [ |xh xl];simpl ww_to_Z;intros H.
    unfold Zlt in H;discriminate H.
-   assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0.
-   destruct (w_compare w_0 xl).
+   rewrite spec_compare, spec_w_0. case Zcompare_spec; intros H0.
    rewrite <- H0; rewrite Zplus_0_r.
    case (spec_to_Z (w_tail0 xh)); intros HH1 HH2.
    generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H.
@@ -323,7 +311,7 @@ Section DoubleLift.
    assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl));
    simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl);
    assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy.
-   generalize (spec_ww_compare p zdigits); case ww_compare; intros H1.
+   rewrite spec_ww_compare; case Zcompare_spec; intros H1.
    rewrite H1; unfold zdigits; rewrite spec_w_0W.
    rewrite spec_zdigits; rewrite Zminus_diag; rewrite Zplus_0_r.
    simpl ww_to_Z; w_rewrite;zarith.
@@ -365,7 +353,7 @@ Section DoubleLift.
    ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith.
    assert (Hv: [[p]] > Zpos w_digits).
      generalize H1; clear H1.
-     unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto.
+     unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto with zarith.
    clear H1.
    assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits).
      rewrite spec_low.
@@ -446,8 +434,7 @@ Section DoubleLift.
     clear H1;w_rewrite);simpl ww_add_mul_div.
    replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial].
    intros Heq;rewrite <- Heq;clear Heq; auto.
-   generalize (spec_ww_compare p (w_0W w_zdigits));
-     case ww_compare; intros H1; w_rewrite.
+   rewrite spec_ww_compare. case Zcompare_spec; intros H1; w_rewrite.
    rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
    generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1.
    assert (HH0: [|low p|] = [[p]]).
@@ -464,7 +451,8 @@ Section DoubleLift.
    rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
    rewrite Zpos_xO in H;zarith.
    assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits).
-     generalize H1; clear H1.
+     symmetry in H1; change ([[p]] > [[w_0W w_zdigits]]) in H1.
+     revert H1.
      rewrite spec_low.
      rewrite spec_ww_sub; w_rewrite; intros H1.
      rewrite <- Zmod_div_mod; auto with zarith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index 834e85d2..0032d2c3 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -248,12 +246,7 @@ Section DoubleMul.
   Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
   Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
   Variable spec_w_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+     forall x y, w_compare x y = Zcompare [|x|] [|y|].
   Variable spec_w_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB.
   Variable spec_w_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
   Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB.
@@ -408,9 +401,9 @@ Section DoubleMul.
      assert (Hyh := (spec_to_Z yh)); assert (Hyl := (spec_to_Z yl)).
    generalize (spec_ww_add_c hh ll); case (ww_add_c hh ll);
      intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)).
-   generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
+   rewrite spec_w_compare; case Zcompare_spec; intros Hxlh;
     try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+   rewrite spec_w_compare; case Zcompare_spec; intros Hylh.
    rewrite Hylh; rewrite spec_w_0; try (ring; fail).
    rewrite spec_w_0; try (ring; fail).
    repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
@@ -430,7 +423,7 @@ Section DoubleMul.
    rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
      repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+   rewrite spec_w_compare; case Zcompare_spec; intros Hylh.
    rewrite Hylh; rewrite spec_w_0; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
      generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0;
@@ -455,9 +448,9 @@ Section DoubleMul.
    apply Zmult_le_0_compat; auto with zarith.
    (** there is a carry in hh + ll **)
    rewrite Zmult_1_l.
-   generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
+   rewrite spec_w_compare; case Zcompare_spec; intros Hxlh;
     try rewrite Hxlh; try rewrite spec_w_1; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
+   rewrite spec_w_compare; case Zcompare_spec; intros Hylh;
      try rewrite Hylh; try rewrite spec_w_1; try (ring; fail).
    match goal with |- context[ww_sub_c ?x ?y] =>
      generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1;
@@ -480,7 +473,7 @@ Section DoubleMul.
    ring.
    rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
+   rewrite spec_w_compare; case Zcompare_spec; intros Hylh;
      try rewrite Hylh; try rewrite spec_w_1; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
      generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1;
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 4394178f..b073d6be 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleSqrt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -220,12 +218,8 @@ Section DoubleSqrt.
   Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
   Variable spec_w_is_even : forall x,
       if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
-   Variable spec_w_compare : forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end.
+  Variable spec_w_compare : forall x y,
+       w_compare x y = Zcompare [|x|] [|y|].
  Variable spec_w_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB.
  Variable spec_w_square_c : forall x, [[ w_square_c x]] = [|x|] * [|x|].
  Variable spec_w_div21 : forall a1 a2 b,
@@ -257,11 +251,7 @@ Section DoubleSqrt.
  Variable spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB.
  Variable spec_ww_add_c  : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
  Variable spec_ww_compare : forall x y,
-       match ww_compare x y with
-       | Eq => [[x]] = [[y]]
-       | Lt => [[x]] < [[y]]
-       | Gt => [[x]] > [[y]]
-       end.
+    ww_compare x y = Zcompare [[x]] [[y]].
  Variable spec_ww_head0  : forall x,  0 < [[x]] ->
 	 wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB.
  Variable spec_low: forall x, [|low x|] = [[x]] mod wB.
@@ -299,10 +289,7 @@ intros x; case x; simpl ww_is_even.
  apply Zlt_le_trans with (2 := Hb); auto with zarith.
  apply Zlt_le_trans with 1; auto with zarith.
  apply Zdiv_le_lower_bound; auto with zarith.
- repeat match goal with |- context[w_compare ?y ?z] =>
-   generalize (spec_w_compare y z);
-   case (w_compare y z)
- end.
+ rewrite !spec_w_compare. repeat case Zcompare_spec.
  intros H1 H2; split.
  unfold interp_carry; autorewrite with w_rewrite rm10; auto with zarith.
  rewrite H1; rewrite H2; ring.
@@ -1108,12 +1095,12 @@ intros x; case x; simpl ww_is_even.
  rewrite wwB_wBwB; rewrite Zpower_2.
  apply Zmult_le_compat_r; auto with zarith.
  case (spec_to_Z w4);auto with zarith.
- Qed.
+Qed.
 
  Lemma spec_ww_is_zero: forall x,
    if ww_is_zero x then [[x]] = 0 else 0 < [[x]].
   intro x; unfold ww_is_zero.
-  generalize (spec_ww_compare W0 x); case (ww_compare W0 x);
+  rewrite spec_ww_compare. case Zcompare_spec;
    auto with zarith.
   simpl ww_to_Z.
   assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z x);auto with zarith.
@@ -1198,7 +1185,7 @@ intros x; case x; simpl ww_is_even.
   simpl ww_to_Z; simpl Zpower; unfold Zpower_pos; simpl;
     auto with zarith.
   intros H1.
-  generalize (spec_ww_compare (ww_head1 x) W0); case ww_compare;
+  rewrite spec_ww_compare. case Zcompare_spec;
     simpl ww_to_Z; autorewrite with rm10.
   generalize H1; case x.
   intros HH; contradict HH; simpl ww_to_Z; auto with zarith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index 3167f4c7..e63e20c6 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleSub.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index eb1132d4..a274b839 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleType.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -55,7 +53,7 @@ Section Zn2Z.
 
 End Zn2Z.
 
-Implicit Arguments W0 [znz].
+Arguments W0 [znz].
 
 (** From a cyclic representation [w], we iterate the [zn2z] construct
     [n] times, gaining the type of binary trees of depth at most [n],
-- 
cgit v1.2.3