1 files changed, 227 insertions, 227 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 0142b36b..180fe0a9 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -21,92 +21,92 @@ Open Scope Z_scope.
   [NSig.NType] to a structure of integers [ZSig.ZType].
 *)
 
-Module Make (N:NType) <: ZType.
+Module Make (NN:NType) <: ZType.
 
  Inductive t_ :=
-  | Pos : N.t -> t_
-  | Neg : N.t -> t_.
+  | Pos : NN.t -> t_
+  | Neg : NN.t -> t_.
 
  Definition t := t_.
 
  Bind Scope abstract_scope with t t_.
 
- Definition zero := Pos N.zero.
- Definition one  := Pos N.one.
- Definition two := Pos N.two.
- Definition minus_one := Neg N.one.
+ Definition zero := Pos NN.zero.
+ Definition one  := Pos NN.one.
+ Definition two := Pos NN.two.
+ Definition minus_one := Neg NN.one.
 
  Definition of_Z x :=
   match x with
-  | Zpos x => Pos (N.of_N (Npos x))
+  | Zpos x => Pos (NN.of_N (Npos x))
   | Z0 => zero
-  | Zneg x => Neg (N.of_N (Npos x))
+  | Zneg x => Neg (NN.of_N (Npos x))
   end.
 
  Definition to_Z x :=
   match x with
-  | Pos nx => N.to_Z nx
-  | Neg nx => Zopp (N.to_Z nx)
+  | Pos nx => NN.to_Z nx
+  | Neg nx => Z.opp (NN.to_Z nx)
   end.
 
  Theorem spec_of_Z: forall x, to_Z (of_Z x) = x.
  Proof.
  intros x; case x; unfold to_Z, of_Z, zero.
-   exact N.spec_0.
-   intros; rewrite N.spec_of_N; auto.
-   intros; rewrite N.spec_of_N; auto.
+   exact NN.spec_0.
+   intros; rewrite NN.spec_of_N; auto.
+   intros; rewrite NN.spec_of_N; auto.
  Qed.
 
  Definition eq x y := (to_Z x = to_Z y).
 
  Theorem spec_0: to_Z zero = 0.
- exact N.spec_0.
+ exact NN.spec_0.
  Qed.
 
  Theorem spec_1: to_Z one = 1.
- exact N.spec_1.
+ exact NN.spec_1.
  Qed.
 
  Theorem spec_2: to_Z two = 2.
- exact N.spec_2.
+ exact NN.spec_2.
  Qed.
 
  Theorem spec_m1: to_Z minus_one = -1.
- simpl; rewrite N.spec_1; auto.
+ simpl; rewrite NN.spec_1; auto.
  Qed.
 
  Definition compare x y :=
   match x, y with
-  | Pos nx, Pos ny => N.compare nx ny
+  | Pos nx, Pos ny => NN.compare nx ny
   | Pos nx, Neg ny =>
-    match N.compare nx N.zero with
+    match NN.compare nx NN.zero with
     | Gt => Gt
-    | _ => N.compare ny N.zero
+    | _ => NN.compare ny NN.zero
     end
   | Neg nx, Pos ny =>
-    match N.compare N.zero nx with
+    match NN.compare NN.zero nx with
     | Lt => Lt
-    | _ => N.compare N.zero ny
+    | _ => NN.compare NN.zero ny
     end
-  | Neg nx, Neg ny => N.compare ny nx
+  | Neg nx, Neg ny => NN.compare ny nx
   end.
 
  Theorem spec_compare :
-  forall x y, compare x y = Zcompare (to_Z x) (to_Z y).
+  forall x y, compare x y = Z.compare (to_Z x) (to_Z y).
  Proof.
  unfold compare, to_Z.
  destruct x as [x|x], y as [y|y];
- rewrite ?N.spec_compare, ?N.spec_0, <-?Zcompare_opp; auto;
- assert (Hx:=N.spec_pos x); assert (Hy:=N.spec_pos y);
- set (X:=N.to_Z x) in *; set (Y:=N.to_Z y) in *; clearbody X Y.
- destruct (Zcompare_spec X 0) as [EQ|LT|GT].
-  rewrite EQ. rewrite <- Zopp_0 at 2. apply Zcompare_opp.
-  exfalso. omega.
-  symmetry. change (X > -Y). omega.
- destruct (Zcompare_spec 0 X) as [EQ|LT|GT].
-  rewrite <- EQ. rewrite Zopp_0; auto.
-  symmetry. change (-X < Y). omega.
-  exfalso. omega.
+ rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto;
+ assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y);
+ set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y.
+ - destruct (Z.compare_spec X 0) as [EQ|LT|GT].
+   + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp.
+   + exfalso. omega.
+   + symmetry. change (X > -Y). omega.
+ - destruct (Z.compare_spec 0 X) as [EQ|LT|GT].
+   + rewrite <- EQ, Z.opp_0; auto.
+   + symmetry. change (-X < Y). omega.
+   + exfalso. omega.
  Qed.
 
  Definition eqb x y :=
@@ -155,14 +155,14 @@ Module Make (N:NType) <: ZType.
  Definition min n m := match compare n m with Gt => m | _ => n end.
  Definition max n m := match compare n m with Lt => m | _ => n end.
 
- Theorem spec_min : forall n m, to_Z (min n m) = Zmin (to_Z n) (to_Z m).
+ Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m).
  Proof.
- unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto.
+ unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto.
  Qed.
 
- Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m).
+ Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m).
  Proof.
- unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto.
+ unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto.
  Qed.
 
  Definition to_N x :=
@@ -173,11 +173,11 @@ Module Make (N:NType) <: ZType.
 
  Definition abs x := Pos (to_N x).
 
- Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x).
+ Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x).
  Proof.
- intros x; case x; clear x; intros x; assert (F:=N.spec_pos x).
-    simpl; rewrite Zabs_eq; auto.
- simpl; rewrite Zabs_non_eq; simpl; auto with zarith.
+ intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x).
+    simpl; rewrite Z.abs_eq; auto.
+ simpl; rewrite Z.abs_neq; simpl; auto with zarith.
  Qed.
 
  Definition opp x :=
@@ -193,10 +193,10 @@ Module Make (N:NType) <: ZType.
 
  Definition succ x :=
   match x with
-  | Pos n => Pos (N.succ n)
+  | Pos n => Pos (NN.succ n)
   | Neg n =>
-    match N.compare N.zero n with
-    | Lt => Neg (N.pred n)
+    match NN.compare NN.zero n with
+    | Lt => Neg (NN.pred n)
     | _ => one
     end
   end.
@@ -204,134 +204,134 @@ Module Make (N:NType) <: ZType.
  Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
  Proof.
  intros x; case x; clear x; intros x.
-   exact (N.spec_succ x).
- simpl. rewrite N.spec_compare. case Zcompare_spec; rewrite ?N.spec_0; simpl.
-  intros HH; rewrite <- HH; rewrite N.spec_1; ring.
-  intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith.
- generalize (N.spec_pos x); auto with zarith.
+   exact (NN.spec_succ x).
+ simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl.
+  intros HH; rewrite <- HH; rewrite NN.spec_1; ring.
+  intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith.
+ generalize (NN.spec_pos x); auto with zarith.
  Qed.
 
  Definition add x y :=
   match x, y with
-  | Pos nx, Pos ny => Pos (N.add nx ny)
+  | Pos nx, Pos ny => Pos (NN.add nx ny)
   | Pos nx, Neg ny =>
-    match N.compare nx ny with
-    | Gt => Pos (N.sub nx ny)
+    match NN.compare nx ny with
+    | Gt => Pos (NN.sub nx ny)
     | Eq => zero
-    | Lt => Neg (N.sub ny nx)
+    | Lt => Neg (NN.sub ny nx)
     end
   | Neg nx, Pos ny =>
-    match N.compare nx ny with
-    | Gt => Neg (N.sub nx ny)
+    match NN.compare nx ny with
+    | Gt => Neg (NN.sub nx ny)
     | Eq => zero
-    | Lt => Pos (N.sub ny nx)
+    | Lt => Pos (NN.sub ny nx)
     end
-  | Neg nx, Neg ny => Neg (N.add nx ny)
+  | Neg nx, Neg ny => Neg (NN.add nx ny)
   end.
 
  Theorem spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
  Proof.
  unfold add, to_Z; intros [x | x] [y | y];
-   try (rewrite N.spec_add; auto with zarith);
- rewrite N.spec_compare; case Zcompare_spec;
-  unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *.
+   try (rewrite NN.spec_add; auto with zarith);
+ rewrite NN.spec_compare; case Z.compare_spec;
+  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *.
  Qed.
 
  Definition pred x :=
   match x with
   | Pos nx =>
-    match N.compare N.zero nx with
-    | Lt => Pos (N.pred nx)
+    match NN.compare NN.zero nx with
+    | Lt => Pos (NN.pred nx)
     | _ => minus_one
     end
-  | Neg nx => Neg (N.succ nx)
+  | Neg nx => Neg (NN.succ nx)
   end.
 
  Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1.
  Proof.
  unfold pred, to_Z, minus_one; intros [x | x];
-   try (rewrite N.spec_succ; ring).
- rewrite N.spec_compare; case Zcompare_spec;
-  rewrite ?N.spec_0, ?N.spec_1, ?N.spec_pred;
-  generalize (N.spec_pos x); omega with *.
+   try (rewrite NN.spec_succ; ring).
+ rewrite NN.spec_compare; case Z.compare_spec;
+  rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred;
+  generalize (NN.spec_pos x); omega with *.
  Qed.
 
  Definition sub x y :=
   match x, y with
   | Pos nx, Pos ny =>
-    match N.compare nx ny with
-    | Gt => Pos (N.sub nx ny)
+    match NN.compare nx ny with
+    | Gt => Pos (NN.sub nx ny)
     | Eq => zero
-    | Lt => Neg (N.sub ny nx)
+    | Lt => Neg (NN.sub ny nx)
     end
-  | Pos nx, Neg ny => Pos (N.add nx ny)
-  | Neg nx, Pos ny => Neg (N.add nx ny)
+  | Pos nx, Neg ny => Pos (NN.add nx ny)
+  | Neg nx, Pos ny => Neg (NN.add nx ny)
   | Neg nx, Neg ny =>
-    match N.compare nx ny with
-    | Gt => Neg (N.sub nx ny)
+    match NN.compare nx ny with
+    | Gt => Neg (NN.sub nx ny)
     | Eq => zero
-    | Lt => Pos (N.sub ny nx)
+    | Lt => Pos (NN.sub ny nx)
     end
   end.
 
  Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y.
  Proof.
  unfold sub, to_Z; intros [x | x] [y | y];
-  try (rewrite N.spec_add; auto with zarith);
- rewrite N.spec_compare; case Zcompare_spec;
-  unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *.
+  try (rewrite NN.spec_add; auto with zarith);
+ rewrite NN.spec_compare; case Z.compare_spec;
+  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *.
  Qed.
 
  Definition mul x y :=
   match x, y with
-  | Pos nx, Pos ny => Pos (N.mul nx ny)
-  | Pos nx, Neg ny => Neg (N.mul nx ny)
-  | Neg nx, Pos ny => Neg (N.mul nx ny)
-  | Neg nx, Neg ny => Pos (N.mul nx ny)
+  | Pos nx, Pos ny => Pos (NN.mul nx ny)
+  | Pos nx, Neg ny => Neg (NN.mul nx ny)
+  | Neg nx, Pos ny => Neg (NN.mul nx ny)
+  | Neg nx, Neg ny => Pos (NN.mul nx ny)
   end.
 
  Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
  Proof.
- unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring.
+ unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring.
  Qed.
 
  Definition square x :=
   match x with
-  | Pos nx => Pos (N.square nx)
-  | Neg nx => Pos (N.square nx)
+  | Pos nx => Pos (NN.square nx)
+  | Neg nx => Pos (NN.square nx)
   end.
 
  Theorem spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
  Proof.
- unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring.
+ unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring.
  Qed.
 
  Definition pow_pos x p :=
   match x with
-  | Pos nx => Pos (N.pow_pos nx p)
+  | Pos nx => Pos (NN.pow_pos nx p)
   | Neg nx =>
     match p with
     | xH => x
-    | xO _ => Pos (N.pow_pos nx p)
-    | xI _ => Neg (N.pow_pos nx p)
+    | xO _ => Pos (NN.pow_pos nx p)
+    | xI _ => Neg (NN.pow_pos nx p)
     end
   end.
 
  Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n.
  Proof.
  assert (F0: forall x, (-x)^2 = x^2).
-   intros x; rewrite Zpower_2; ring.
+   intros x; rewrite Z.pow_2_r; ring.
  unfold pow_pos, to_Z; intros [x | x] [p | p |];
-   try rewrite N.spec_pow_pos; try ring.
+   try rewrite NN.spec_pow_pos; try ring.
  assert (F: 0 <= 2 * Zpos p).
   assert (0 <= Zpos p); auto with zarith.
- rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith.
- repeat rewrite Zpower_mult; auto with zarith.
+ rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith.
+ repeat rewrite Z.pow_mul_r; auto with zarith.
  rewrite F0; ring.
  assert (F: 0 <= 2 * Zpos p).
   assert (0 <= Zpos p); auto with zarith.
- rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith.
- repeat rewrite Zpower_mult; auto with zarith.
+ rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith.
+ repeat rewrite Z.pow_mul_r; auto with zarith.
  rewrite F0; ring.
  Qed.
 
@@ -341,9 +341,9 @@ Module Make (N:NType) <: ZType.
   | Npos p => pow_pos x p
   end.
 
- Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n.
+ Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n.
  Proof.
- destruct n; simpl. apply N.spec_1.
+ destruct n; simpl. apply NN.spec_1.
  apply spec_pow_pos.
  Qed.
 
@@ -357,38 +357,38 @@ Module Make (N:NType) <: ZType.
  Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y.
  Proof.
  intros. unfold pow. destruct (to_Z y); simpl.
- apply N.spec_1.
+ apply NN.spec_1.
  apply spec_pow_pos.
- apply N.spec_0.
+ apply NN.spec_0.
  Qed.
 
  Definition log2 x :=
   match x with
-  | Pos nx => Pos (N.log2 nx)
+  | Pos nx => Pos (NN.log2 nx)
   | Neg nx => zero
   end.
 
  Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x).
  Proof.
-  intros. destruct x as [p|p]; simpl. apply N.spec_log2.
-  rewrite N.spec_0.
-  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  intros. destruct x as [p|p]; simpl. apply NN.spec_log2.
+  rewrite NN.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ].
   rewrite Z.log2_nonpos; auto with zarith.
   now rewrite <- EQ.
  Qed.
 
  Definition sqrt x :=
   match x with
-  | Pos nx => Pos (N.sqrt nx)
-  | Neg nx => Neg N.zero
+  | Pos nx => Pos (NN.sqrt nx)
+  | Neg nx => Neg NN.zero
   end.
 
  Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x).
  Proof.
   destruct x as [p|p]; simpl.
-  apply N.spec_sqrt.
-  rewrite N.spec_0.
-  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  apply NN.spec_sqrt.
+  rewrite NN.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ].
   rewrite Z.sqrt_neg; auto with zarith.
   now rewrite <- EQ.
  Qed.
@@ -396,68 +396,68 @@ Module Make (N:NType) <: ZType.
  Definition div_eucl x y :=
   match x, y with
   | Pos nx, Pos ny =>
-    let (q, r) := N.div_eucl nx ny in
+    let (q, r) := NN.div_eucl nx ny in
     (Pos q, Pos r)
   | Pos nx, Neg ny =>
-    let (q, r) := N.div_eucl nx ny in
-    if N.eqb N.zero r
+    let (q, r) := NN.div_eucl nx ny in
+    if NN.eqb NN.zero r
     then (Neg q, zero)
-    else (Neg (N.succ q), Neg (N.sub ny r))
+    else (Neg (NN.succ q), Neg (NN.sub ny r))
   | Neg nx, Pos ny =>
-    let (q, r) := N.div_eucl nx ny in
-    if N.eqb N.zero r
+    let (q, r) := NN.div_eucl nx ny in
+    if NN.eqb NN.zero r
     then (Neg q, zero)
-    else (Neg (N.succ q), Pos (N.sub ny r))
+    else (Neg (NN.succ q), Pos (NN.sub ny r))
   | Neg nx, Neg ny =>
-    let (q, r) := N.div_eucl nx ny in
+    let (q, r) := NN.div_eucl nx ny in
     (Pos q, Neg r)
   end.
 
  Ltac break_nonneg x px EQx :=
   let H := fresh "H" in
-  assert (H:=N.spec_pos x);
-  destruct (N.to_Z x) as [|px|px]_eqn:EQx;
+  assert (H:=NN.spec_pos x);
+  destruct (NN.to_Z x) as [|px|px] eqn:EQx;
    [clear H|clear H|elim H; reflexivity].
 
  Theorem spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in
-   (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
+   (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y).
  Proof.
  unfold div_eucl, to_Z. intros [x | x] [y | y].
  (* Pos Pos *)
- generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y); auto.
+ generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto.
  (* Pos Neg *)
- generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
-      simpl; rewrite Hq, N.spec_0; auto).
+ try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+      simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos py) with (Zneg py).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
- unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
+ unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eqb, N.spec_0, Hr'.
+ rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
- subst; simpl. rewrite N.spec_0; auto.
+ subst; simpl. rewrite NN.spec_0; auto.
  subst. lazy iota beta delta [Z.eqb].
- rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
+ rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Pos *)
- generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
-      simpl; rewrite Hq, N.spec_0; auto).
+ try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+      simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos px) with (Zneg px).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
- unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
+ unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eqb, N.spec_0, Hr'.
+ rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
- subst; simpl. rewrite N.spec_0; auto.
+ subst; simpl. rewrite NN.spec_0; auto.
  subst. lazy iota beta delta [Z.eqb].
- rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
+ rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Neg *)
- generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
  try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto).
  simpl. intros <-; auto.
@@ -468,8 +468,8 @@ Module Make (N:NType) <: ZType.
  Definition spec_div: forall x y,
      to_Z (div x y) = to_Z x / to_Z y.
  Proof.
- intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv.
- case div_eucl; case Zdiv_eucl; simpl; auto.
+ intros x y; generalize (spec_div_eucl x y); unfold div, Z.div.
+ case div_eucl; case Z.div_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
  Qed.
 
@@ -478,38 +478,38 @@ Module Make (N:NType) <: ZType.
  Theorem spec_modulo:
    forall x y, to_Z (modulo x y) = to_Z x mod to_Z y.
  Proof.
- intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod.
- case div_eucl; case Zdiv_eucl; simpl; auto.
+ intros x y; generalize (spec_div_eucl x y); unfold modulo, Z.modulo.
+ case div_eucl; case Z.div_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
  Qed.
 
  Definition quot x y :=
   match x, y with
-  | Pos nx, Pos ny => Pos (N.div nx ny)
-  | Pos nx, Neg ny => Neg (N.div nx ny)
-  | Neg nx, Pos ny => Neg (N.div nx ny)
-  | Neg nx, Neg ny => Pos (N.div nx ny)
+  | Pos nx, Pos ny => Pos (NN.div nx ny)
+  | Pos nx, Neg ny => Neg (NN.div nx ny)
+  | Neg nx, Pos ny => Neg (NN.div nx ny)
+  | Neg nx, Neg ny => Pos (NN.div nx ny)
   end.
 
  Definition rem x y :=
   if eqb y zero then x
   else
     match x, y with
-      | Pos nx, Pos ny => Pos (N.modulo nx ny)
-      | Pos nx, Neg ny => Pos (N.modulo nx ny)
-      | Neg nx, Pos ny => Neg (N.modulo nx ny)
-      | Neg nx, Neg ny => Neg (N.modulo nx ny)
+      | Pos nx, Pos ny => Pos (NN.modulo nx ny)
+      | Pos nx, Neg ny => Pos (NN.modulo nx ny)
+      | Neg nx, Pos ny => Neg (NN.modulo nx ny)
+      | Neg nx, Neg ny => Neg (NN.modulo nx ny)
     end.
 
  Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
  Proof.
-  intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div;
+  intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div;
   (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *)
-  destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ];
-    try (rewrite EQ; now destruct (N.to_Z x));
+  destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ];
+    try (rewrite EQ; now destruct (NN.to_Z x));
   rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd;
   trivial; apply Z.quot_div_nonneg;
-   generalize (N.spec_pos x) (N.spec_pos y); Z.order.
+   generalize (NN.spec_pos x) (NN.spec_pos y); Z.order.
  Qed.
 
  Lemma spec_rem : forall x y,
@@ -521,26 +521,26 @@ Module Make (N:NType) <: ZType.
   rewrite Hy. now destruct (to_Z x).
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
    rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy;
-   rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive,
+   rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive,
     ?Z.opp_inj_wd;
    trivial; apply Z.rem_mod_nonneg;
-    generalize (N.spec_pos x) (N.spec_pos y); Z.order.
+    generalize (NN.spec_pos x) (NN.spec_pos y); Z.order.
  Qed.
 
  Definition gcd x y :=
   match x, y with
-  | Pos nx, Pos ny => Pos (N.gcd nx ny)
-  | Pos nx, Neg ny => Pos (N.gcd nx ny)
-  | Neg nx, Pos ny => Pos (N.gcd nx ny)
-  | Neg nx, Neg ny => Pos (N.gcd nx ny)
+  | Pos nx, Pos ny => Pos (NN.gcd nx ny)
+  | Pos nx, Neg ny => Pos (NN.gcd nx ny)
+  | Neg nx, Pos ny => Pos (NN.gcd nx ny)
+  | Neg nx, Neg ny => Pos (NN.gcd nx ny)
   end.
 
- Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
+ Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b).
  Proof.
- unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd;
-  auto; case N.to_Z; simpl; auto with zarith;
-  try rewrite Zabs_Zopp; auto;
-  case N.to_Z; simpl; auto with zarith.
+ unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd;
+  auto; case NN.to_Z; simpl; auto with zarith;
+  try rewrite Z.abs_opp; auto;
+  case NN.to_Z; simpl; auto with zarith.
  Qed.
 
  Definition sgn x :=
@@ -550,124 +550,124 @@ Module Make (N:NType) <: ZType.
    | Gt => minus_one
   end.
 
- Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x).
+ Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x).
  Proof.
- intros. unfold sgn. rewrite spec_compare. case Zcompare_spec.
+ intros. unfold sgn. rewrite spec_compare. case Z.compare_spec.
  rewrite spec_0. intros <-; auto.
- rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto.
- rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith.
+ rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto.
+ rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith.
  Qed.
 
  Definition even z :=
   match z with
-   | Pos n => N.even n
-   | Neg n => N.even n
+   | Pos n => NN.even n
+   | Neg n => NN.even n
   end.
 
  Definition odd z :=
   match z with
-   | Pos n => N.odd n
-   | Neg n => N.odd n
+   | Pos n => NN.odd n
+   | Neg n => NN.odd n
   end.
 
- Lemma spec_even : forall z, even z = Zeven_bool (to_Z z).
+ Lemma spec_even : forall z, even z = Z.even (to_Z z).
  Proof.
-  intros [n|n]; simpl; rewrite N.spec_even; trivial.
-  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+  intros [n|n]; simpl; rewrite NN.spec_even; trivial.
+  destruct (NN.to_Z n) as [|p|p]; now try destruct p.
  Qed.
 
- Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z).
+ Lemma spec_odd : forall z, odd z = Z.odd (to_Z z).
  Proof.
-  intros [n|n]; simpl; rewrite N.spec_odd; trivial.
-  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+  intros [n|n]; simpl; rewrite NN.spec_odd; trivial.
+  destruct (NN.to_Z n) as [|p|p]; now try destruct p.
  Qed.
 
  Definition norm_pos z :=
    match z with
      | Pos _ => z
-     | Neg n => if N.eqb n N.zero then Pos n else z
+     | Neg n => if NN.eqb n NN.zero then Pos n else z
    end.
 
  Definition testbit a n :=
    match norm_pos n, norm_pos a with
-     | Pos p, Pos a => N.testbit a p
-     | Pos p, Neg a => negb (N.testbit (N.pred a) p)
+     | Pos p, Pos a => NN.testbit a p
+     | Pos p, Neg a => negb (NN.testbit (NN.pred a) p)
      | Neg p, _ => false
    end.
 
  Definition shiftl a n :=
    match norm_pos a, n with
-     | Pos a, Pos n => Pos (N.shiftl a n)
-     | Pos a, Neg n => Pos (N.shiftr a n)
-     | Neg a, Pos n => Neg (N.shiftl a n)
-     | Neg a, Neg n => Neg (N.succ (N.shiftr (N.pred a) n))
+     | Pos a, Pos n => Pos (NN.shiftl a n)
+     | Pos a, Neg n => Pos (NN.shiftr a n)
+     | Neg a, Pos n => Neg (NN.shiftl a n)
+     | Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n))
    end.
 
  Definition shiftr a n := shiftl a (opp n).
 
  Definition lor a b :=
    match norm_pos a, norm_pos b with
-     | Pos a, Pos b => Pos (N.lor a b)
-     | Neg a, Pos b => Neg (N.succ (N.ldiff (N.pred a) b))
-     | Pos a, Neg b => Neg (N.succ (N.ldiff (N.pred b) a))
-     | Neg a, Neg b => Neg (N.succ (N.land (N.pred a) (N.pred b)))
+     | Pos a, Pos b => Pos (NN.lor a b)
+     | Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b))
+     | Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a))
+     | Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b)))
    end.
 
  Definition land a b :=
    match norm_pos a, norm_pos b with
-     | Pos a, Pos b => Pos (N.land a b)
-     | Neg a, Pos b => Pos (N.ldiff b (N.pred a))
-     | Pos a, Neg b => Pos (N.ldiff a (N.pred b))
-     | Neg a, Neg b => Neg (N.succ (N.lor (N.pred a) (N.pred b)))
+     | Pos a, Pos b => Pos (NN.land a b)
+     | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a))
+     | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b))
+     | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b)))
    end.
 
  Definition ldiff a b :=
    match norm_pos a, norm_pos b with
-     | Pos a, Pos b => Pos (N.ldiff a b)
-     | Neg a, Pos b => Neg (N.succ (N.lor (N.pred a) b))
-     | Pos a, Neg b => Pos (N.land a (N.pred b))
-     | Neg a, Neg b => Pos (N.ldiff (N.pred b) (N.pred a))
+     | Pos a, Pos b => Pos (NN.ldiff a b)
+     | Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b))
+     | Pos a, Neg b => Pos (NN.land a (NN.pred b))
+     | Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a))
    end.
 
  Definition lxor a b :=
    match norm_pos a, norm_pos b with
-     | Pos a, Pos b => Pos (N.lxor a b)
-     | Neg a, Pos b => Neg (N.succ (N.lxor (N.pred a) b))
-     | Pos a, Neg b => Neg (N.succ (N.lxor a (N.pred b)))
-     | Neg a, Neg b => Pos (N.lxor (N.pred a) (N.pred b))
+     | Pos a, Pos b => Pos (NN.lxor a b)
+     | Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b))
+     | Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b)))
+     | Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b))
    end.
 
  Definition div2 x := shiftr x one.
 
  Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x.
  Proof.
-  unfold Z.lnot, Zpred; auto with zarith.
+  unfold Z.lnot, Z.pred; auto with zarith.
  Qed.
 
  Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x.
  Proof.
-  unfold Z.lnot, Zpred; auto with zarith.
+  unfold Z.lnot, Z.pred; auto with zarith.
  Qed.
 
  Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1.
  Proof.
-  unfold Z.lnot, Zpred; auto with zarith.
+  unfold Z.lnot, Z.pred; auto with zarith.
  Qed.
 
  Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
  Proof.
   intros [x|x]; simpl; trivial.
-  rewrite N.spec_eqb, N.spec_0.
+  rewrite NN.spec_eqb, NN.spec_0.
   case Z.eqb_spec; simpl; auto with zarith.
  Qed.
 
  Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
-  0 < N.to_Z y.
+  0 < NN.to_Z y.
  Proof.
   intros [x|x] y; simpl; try easy.
-  rewrite N.spec_eqb, N.spec_0.
+  rewrite NN.spec_eqb, NN.spec_0.
   case Z.eqb_spec; simpl; try easy.
-  inversion 2. subst. generalize (N.spec_pos y); auto with zarith.
+  inversion 2. subst. generalize (NN.spec_pos y); auto with zarith.
  Qed.
 
  Ltac destr_norm_pos x :=
@@ -682,9 +682,9 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x p. unfold testbit.
   destr_norm_pos p; simpl. destr_norm_pos x; simpl.
-  apply N.spec_testbit.
-  rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith.
-  symmetry. apply Z.bits_opp. apply N.spec_pos.
+  apply NN.spec_testbit.
+  rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith.
+  symmetry. apply Z.bits_opp. apply NN.spec_pos.
   symmetry. apply Z.testbit_neg_r; auto with zarith.
  Qed.
 
@@ -692,13 +692,13 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x p. unfold shiftl.
   destr_norm_pos x; destruct p as [p|p]; simpl;
-   assert (Hp := N.spec_pos p).
-  apply N.spec_shiftl.
-  rewrite Z.shiftl_opp_r. apply N.spec_shiftr.
-  rewrite !N.spec_shiftl.
-  rewrite !Z.shiftl_mul_pow2 by apply N.spec_pos.
-  apply Zopp_mult_distr_l.
-  rewrite Z.shiftl_opp_r, N.spec_succ, N.spec_shiftr, N.spec_pred, Zmax_r
+   assert (Hp := NN.spec_pos p).
+  apply NN.spec_shiftl.
+  rewrite Z.shiftl_opp_r. apply NN.spec_shiftr.
+  rewrite !NN.spec_shiftl.
+  rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos.
+  symmetry. apply Z.mul_opp_l.
+  rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r
    by auto with zarith.
   now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2.
  Qed.
@@ -713,8 +713,8 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x y. unfold land.
   destr_norm_pos x; destr_norm_pos y; simpl;
-   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
-    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+   rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor,
+    ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith.
   now rewrite Z.ldiff_land, Zlnot_alt2.
   now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2.
   now rewrite Z.lnot_lor, !Zlnot_alt2.
@@ -724,8 +724,8 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x y. unfold lor.
   destr_norm_pos x; destr_norm_pos y; simpl;
-   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
-    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+   rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor,
+    ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith.
   now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2.
   now rewrite Z.lnot_ldiff, Zlnot_alt2.
   now rewrite Z.lnot_land, !Zlnot_alt2.
@@ -735,8 +735,8 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x y. unfold ldiff.
   destr_norm_pos x; destr_norm_pos y; simpl;
-   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
-    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+   rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor,
+    ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith.
   now rewrite Z.ldiff_land, Zlnot_alt3.
   now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2.
   now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3.
@@ -746,7 +746,7 @@ Module Make (N:NType) <: ZType.
  Proof.
   intros x y. unfold lxor.
   destr_norm_pos x; destr_norm_pos y; simpl;
-   rewrite ?N.spec_succ, ?N.spec_lxor, ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1;
+   rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1;
    auto with zarith.
   now rewrite !Z.lnot_lxor_r, Zlnot_alt2.
   now rewrite !Z.lnot_lxor_l, Zlnot_alt2.