Imported Upstream version 8.4dfsgupstream/8.4dfsg

28 files changed, 272 insertions, 282 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 72e09f15..0ff86fca 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index da41886f..5f80714a 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index ca6ccc1b..061da038 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index ac8a0522..09e9ccdf 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index c66f003e..1581ce57 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.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        *)
@@ -236,7 +236,7 @@ Proof.
 Qed.
 
 (** Hence the number of bits of [a] is [1+log2 a]
-    (see [Psize] and [Psize_pos]).
+    (see [Pos.size_nat] and [Pos.size]).
 *)
 
 (** Testing bits after division or multiplication by a power of two *)
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index ad7a9f3a..621a2ed9 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.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        *)
@@ -376,7 +376,7 @@ Lemma log_good_step : forall n h1 h2,
   (if n << 2 then 0 else S (h2 (half n))).
 Proof.
 intros n h1 h2 E.
-destruct (n<<2) as [ ]_eqn:H.
+destruct (n<<2) eqn:H.
 auto with *.
 f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 6db8e448..d7fb447e 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index ece369d8..1c5829dd 100644
--- a/theories/Numbers/Natural/Abstract/NGcd.v
+++ b/theories/Numbers/Natural/Abstract/NGcd.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index bcf746a7..b17f0c3d 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 1e8e678c..9d8e3e6d 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v
index 74827c6e..f8dc1a2b 100644
--- a/theories/Numbers/Natural/Abstract/NLog.v
+++ b/theories/Numbers/Natural/Abstract/NLog.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v
index cdff6dbc..dde7aba5 100644
--- a/theories/Numbers/Natural/Abstract/NMaxMin.v
+++ b/theories/Numbers/Natural/Abstract/NMaxMin.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 1d6e8ba0..2f4c91e3 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 8bba7d72..a5a12d37 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index 6a1e20ce..69b7778a 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 07aee9c6..ee29a4a7 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 1edb6b51..90739410 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 34b7d011..9cd62ae9 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 607746d5..e4cbf090 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.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        *)
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index d7143c67..68bfffad 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.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        *)
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 7f205b38..072b75f7 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.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        *)
@@ -119,7 +119,7 @@ BigN.zify. auto with zarith.
 intros NEQ.
 generalize (BigN.spec_div_eucl a b).
 generalize (Z_div_mod_full [a] [b] NEQ).
-destruct BigN.div_eucl as (q,r), Zdiv_eucl as (q',r').
+destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
 intros (EQ,_). injection 1. intros EQr EQq.
 BigN.zify. rewrite EQr, EQq; auto.
 Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 952f6183..5012a1b9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.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        *)
@@ -65,8 +65,8 @@ Module Make (W0:CyclicType) <: NType.
  intros.
  change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))).
  rewrite !digits_dom_op, !Pshiftl_nat_Zpower.
- apply Zmult_le_compat_l; auto with zarith.
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.mul_le_mono_nonneg_l; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
  Qed.
 
  Definition to_N (x : t) := Z.to_N (to_Z x).
@@ -186,12 +186,12 @@ Module Make (W0:CyclicType) <: NType.
   exact spec_0.
  Qed.
 
- Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1).
+ Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1).
  Proof.
- intros. destruct (Zle_lt_or_eq _ _ (spec_pos x)).
- rewrite Zmax_r; auto with zarith.
- apply spec_pred_pos; auto.
- rewrite <- H; apply spec_pred0; auto.
+ rewrite Z.max_comm.
+ destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)].
+ - apply spec_pred0; generalize (spec_pos x); auto with zarith.
+ - apply spec_pred_pos; auto with zarith.
  Qed.
 
  (** * Subtraction *)
@@ -230,11 +230,11 @@ Module Make (W0:CyclicType) <: NType.
   exact spec_0.
  Qed.
 
- Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]).
+ Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]).
  Proof.
- intros. destruct (Zle_or_lt [y] [x]).
- rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto.
- rewrite Zmax_l; auto with zarith. apply spec_sub0; auto.
+ intros. destruct (Z.le_gt_cases [y] [x]).
+ rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto.
+ rewrite Z.max_l; auto with zarith. apply spec_sub0; auto.
  Qed.
 
  (** * Comparison *)
@@ -249,7 +249,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Let spec_comparen_m:
   forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
-   comparen_m n m x y = Zcompare (eval n (S m) x) (ZnZ.to_Z y).
+   comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
  Proof.
   intros n m x y.
   unfold comparen_m, eval.
@@ -287,10 +287,8 @@ Module Make (W0:CyclicType) <: NType.
  lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity.
  Qed.
 
-(** TODO: no need for ZnZ.Spec_rect , Spec_ind, and so on... *)
-
  Theorem spec_compare : forall x y,
-   compare x y = Zcompare [x] [y].
+   compare x y = Z.compare [x] [y].
  Proof.
   intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y.
   intros. apply ZnZ.spec_compare.
@@ -298,7 +296,7 @@ Module Make (W0:CyclicType) <: NType.
   intros n m x y; unfold comparenm.
   rewrite (spec_cast_l n m x), (spec_cast_r n m y).
   unfold to_Z; apply ZnZ.spec_compare.
-  intros. subst. apply Zcompare_antisym.
+  intros. subst. now rewrite <- Z.compare_antisym.
  Qed.
 
  Definition eqb (x y : t) : bool :=
@@ -346,14 +344,14 @@ Module Make (W0:CyclicType) <: NType.
  Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
  Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
 
- Theorem spec_max : forall n m, [max n m] = Zmax [n] [m].
+ Theorem spec_max : forall n m, [max n m] = Z.max [n] [m].
  Proof.
- intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity.
+ intros. unfold max, Z.max. rewrite spec_compare; destruct Z.compare; reflexivity.
  Qed.
 
- Theorem spec_min : forall n m, [min n m] = Zmin [n] [m].
+ Theorem spec_min : forall n m, [min n m] = Z.min [n] [m].
  Proof.
- intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity.
+ intros. unfold min, Z.min. rewrite spec_compare; destruct Z.compare; reflexivity.
  Qed.
 
  (** * Multiplication *)
@@ -437,7 +435,7 @@ Module Make (W0:CyclicType) <: NType.
   intros; unfold wn_mul.
   generalize (spec_mul_add_n1 n m x y ZnZ.zero).
   case DoubleMul.double_mul_add_n1; intros q r Hqr.
-  rewrite ZnZ.spec_0, Zplus_0_r in Hqr. rewrite <- Hqr.
+  rewrite ZnZ.spec_0, Z.add_0_r in Hqr. rewrite <- Hqr.
   generalize (ZnZ.spec_eq0 q); case ZnZ.eq0; intros HH.
   rewrite HH; auto. simpl. apply spec_mk_t_w'.
   clear.
@@ -458,7 +456,7 @@ Module Make (W0:CyclicType) <: NType.
    intros n m x y; unfold mulnm. rewrite spec_reduce_n.
     rewrite (spec_cast_l n m x), (spec_cast_r n m y).
     apply spec_muln.
-   intros. rewrite Zmult_comm; auto.
+   intros. rewrite Z.mul_comm; auto.
  Qed.
 
  (** * Division by a smaller number *)
@@ -519,7 +517,7 @@ Module Make (W0:CyclicType) <: NType.
   apply DoubleBase.spec_get_low.
   apply spec_zeron.
   exact ZnZ.spec_to_Z.
-  apply Zle_lt_trans with (ZnZ.to_Z y); auto.
+  apply Z.le_lt_trans with (ZnZ.to_Z y); auto.
     rewrite <- nmake_double; auto.
   case (ZnZ.spec_to_Z y); auto.
  Qed.
@@ -580,9 +578,9 @@ Module Make (W0:CyclicType) <: NType.
   intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt.
   intros q r (H3, H4); split.
   apply (Zdiv_unique [x] [y] [q] [r]); auto.
-  rewrite Zmult_comm; auto.
+  rewrite Z.mul_comm; auto.
   apply (Zmod_unique [x] [y] [q] [r]); auto.
-  rewrite Zmult_comm; auto.
+  rewrite Z.mul_comm; auto.
  Qed.
 
  (** * General Division *)
@@ -597,7 +595,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Theorem spec_div_eucl: forall x y,
       let (q,r) := div_eucl x y in
-      ([q], [r]) = Zdiv_eucl [x] [y].
+      ([q], [r]) = Z.div_eucl [x] [y].
  Proof.
  intros x y. unfold div_eucl.
  rewrite spec_eqb, spec_compare, spec_0.
@@ -606,16 +604,16 @@ Module Make (W0:CyclicType) <: NType.
  intros H'.
  assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
  clear H'.
- case Zcompare_spec; intros Cmp;
+ case Z.compare_spec; intros Cmp;
    rewrite ?spec_0, ?spec_1; intros; auto with zarith.
- rewrite Cmp; generalize (Z_div_same [y] (Zlt_gt _ _ H))
-                         (Z_mod_same [y] (Zlt_gt _ _ H));
-  unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.
+ rewrite Cmp; generalize (Z_div_same [y] (Z.lt_gt _ _ H))
+                         (Z_mod_same [y] (Z.lt_gt _ _ H));
+  unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto.
  assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto).
  generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt);
-  unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.
- generalize (spec_div_gt _ _ (Zlt_gt _ _ Cmp) H); auto.
- unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt.
+  unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto.
+ generalize (spec_div_gt _ _ (Z.lt_gt _ _ Cmp) H); auto.
+ unfold Z.div, Z.modulo; case Z.div_eucl; case div_gt.
  intros a b c d (H1, H2); subst; auto.
  Qed.
 
@@ -626,7 +624,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros x y; unfold div; generalize (spec_div_eucl x y);
    case div_eucl; simpl fst.
- intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H;
+ intros xx yy; unfold Z.div; case Z.div_eucl; intros qq rr H;
   injection H; auto.
  Qed.
 
@@ -730,10 +728,10 @@ Module Make (W0:CyclicType) <: NType.
  intro H'.
  assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
  clear H'.
- case Zcompare_spec;
+ case Z.compare_spec;
    rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith.
- rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.
- apply sym_equal; apply Zmod_small; auto with zarith.
+ rewrite H0; symmetry; apply Z_mod_same; auto with zarith.
+ symmetry; apply Zmod_small; auto with zarith.
  generalize (spec_pos x); auto with zarith.
  apply spec_mod_gt; auto with zarith.
  Qed.
@@ -775,7 +773,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
   intros x.
   symmetry. apply Z.sqrt_unique.
-  rewrite <- ! Zpower_2. apply spec_sqrt_aux.
+  rewrite <- ! Z.pow_2_r. apply spec_sqrt_aux.
  Qed.
 
  (** * Power *)
@@ -791,14 +789,14 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros x n; generalize x; elim n; clear n x; simpl pow_pos.
  intros; rewrite spec_mul; rewrite spec_square; rewrite H.
- rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.
- rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
- rewrite Zpower_2; rewrite Zpower_1_r; auto.
+ rewrite Pos2Z.inj_xI; rewrite Zpower_exp; auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r; rewrite Z.pow_1_r; auto.
  intros; rewrite spec_square; rewrite H.
- rewrite Zpos_xO; auto with zarith.
- rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
- rewrite Zpower_2; auto.
- intros; rewrite Zpower_1_r; auto.
+ rewrite Pos2Z.inj_xO; auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r; auto.
+ intros; rewrite Z.pow_1_r; auto.
  Qed.
 
  Definition pow_N (x:t)(n:N) : t := match n with
@@ -806,7 +804,7 @@ Module Make (W0:CyclicType) <: NType.
   | BinNat.Npos p => pow_pos x p
  end.
 
- Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
+ Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.
  Proof.
  destruct n; simpl. apply spec_1.
  apply spec_pow_pos.
@@ -867,15 +865,15 @@ Module Make (W0:CyclicType) <: NType.
       Zis_gcd [a] [b] [gcd_gt_body a b cont].
  Proof.
  intros a b cont p H2 H3 H4; unfold gcd_gt_body.
- rewrite ! spec_compare, spec_0. case Zcompare_spec.
+ rewrite ! spec_compare, spec_0. case Z.compare_spec.
   intros ->; apply Zis_gcd_0.
  intros HH; absurd (0 <= [b]); auto with zarith.
  case (spec_digits b); auto with zarith.
- intros H5; case Zcompare_spec.
- intros H6; rewrite <- (Zmult_1_r [b]).
+ intros H5; case Z.compare_spec.
+ intros H6; rewrite <- (Z.mul_1_r [b]).
  rewrite (Z_div_mod_eq [a] [b]); auto with zarith.
  rewrite <- spec_mod_gt; auto with zarith.
- rewrite H6; rewrite Zplus_0_r.
+ rewrite H6; rewrite Z.add_0_r.
  apply Zis_gcd_mult; apply Zis_gcd_1.
  intros; apply False_ind.
  case (spec_digits (mod_gt a b)); auto with zarith.
@@ -890,24 +888,19 @@ Module Make (W0:CyclicType) <: NType.
    rewrite <- spec_mod_gt; auto with zarith.
  repeat rewrite <- spec_mod_gt; auto with zarith.
  apply H4; auto with zarith.
- apply Zmult_lt_reg_r with 2; auto with zarith.
- apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith.
- apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith.
-   apply Zplus_le_compat_r.
- pattern [b] at 1; rewrite <- (Zmult_1_l [b]).
- apply Zmult_le_compat_r; auto with zarith.
- case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith.
- intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2;
-   try rewrite <- HH in H2; auto with zarith.
- case (Z_mod_lt [a] [b]); auto with zarith.
- rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith.
- rewrite <- Z_div_mod_eq; auto with zarith.
- pattern 2 at 2; rewrite <- (Zpower_1_r 2).
- rewrite <- Zpower_exp; auto with zarith.
- ring_simplify (p - 1 + 1); auto.
- case (Zle_lt_or_eq 0 p); auto with zarith.
- generalize H3; case p; simpl Zpower; auto with zarith.
- intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith.
+ apply Z.mul_lt_mono_pos_r with 2; auto with zarith.
+ apply Z.le_lt_trans with ([b] + [mod_gt a b]); auto with zarith.
+ apply Z.le_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith.
+ - apply Z.add_le_mono_r.
+   rewrite <- (Z.mul_1_l [b]) at 1.
+   apply Z.mul_le_mono_nonneg_r; auto with zarith.
+   change 1 with (Z.succ 0). apply Z.le_succ_l.
+   apply Z.div_str_pos; auto with zarith.
+ - rewrite Z.mul_comm; rewrite spec_mod_gt; auto with zarith.
+   rewrite <- Z_div_mod_eq; auto with zarith.
+   rewrite Z.mul_comm, <- Z.pow_succ_r, Z.sub_1_r, Z.succ_pred; auto.
+   apply Z.le_0_sub. change 1 with (Z.succ 0). apply Z.le_succ_l.
+   destruct p; simpl in H3; auto with zarith.
  Qed.
 
  Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t :=
@@ -931,7 +924,7 @@ Module Make (W0:CyclicType) <: NType.
      apply Hrec with (Zpos p + n); auto.
        replace (Zpos p + (Zpos p + n)) with
          (Zpos (xI p) + n  - 1); auto.
-       rewrite Zpos_xI; ring.
+       rewrite Pos2Z.inj_xI; ring.
    intros a2 b2 H9 H10.
      apply Hrec with n; auto.
  intros p Hrec n a b cont H2 H3 H4.
@@ -940,18 +933,18 @@ Module Make (W0:CyclicType) <: NType.
      apply Hrec with (Zpos p + n - 1); auto.
        replace (Zpos p + (Zpos p + n - 1)) with
          (Zpos (xO p) + n  - 1); auto.
-       rewrite Zpos_xO; ring.
+       rewrite Pos2Z.inj_xO; ring.
    intros a2 b2 H9 H10.
      apply Hrec with (n - 1); auto.
        replace (Zpos p + (n - 1)) with
          (Zpos p + n  - 1); auto with zarith.
    intros a3 b3 H12 H13; apply H4; auto with zarith.
-    apply Zlt_le_trans with (1 := H12).
-    apply Zpower_le_monotone2; auto with zarith.
+    apply Z.lt_le_trans with (1 := H12).
+    apply Z.pow_le_mono_r; auto with zarith.
  intros n a b cont H H2 H3.
   simpl gcd_gt_aux.
   apply Zspec_gcd_gt_body with (n + 1); auto with zarith.
-  rewrite Zplus_comm; auto.
+  rewrite Z.add_comm; auto.
   intros a1 b1 H5 H6; apply H3; auto.
   replace n with (n + 1 - 1); auto; try ring.
  Qed.
@@ -965,14 +958,14 @@ Module Make (W0:CyclicType) <: NType.
  Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.
 
  Theorem spec_gcd_gt: forall a b,
-   [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b].
+   [a] > [b] -> [gcd_gt a b] = Z.gcd [a] [b].
  Proof.
  intros a b H2.
  case (spec_digits (gcd_gt a b)); intros H3 H4.
  case (spec_digits a); intros H5 H6.
- apply sym_equal; apply Zis_gcd_gcd; auto with zarith.
+ symmetry; apply Zis_gcd_gcd; auto with zarith.
  unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith.
- intros a1 a2; rewrite Zpower_0_r.
+ intros a1 a2; rewrite Z.pow_0_r.
  case (spec_digits a2); intros H7 H8;
    intros; apply False_ind; auto with zarith.
  Qed.
@@ -984,18 +977,18 @@ Module Make (W0:CyclicType) <: NType.
   | Gt => gcd_gt a b
   end.
 
- Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
+ Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
  Proof.
  intros a b.
  case (spec_digits a); intros H1 H2.
  case (spec_digits b); intros H3 H4.
- unfold gcd. rewrite spec_compare. case Zcompare_spec.
- intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto.
+ unfold gcd. rewrite spec_compare. case Z.compare_spec.
+ intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto.
    apply Zis_gcd_refl.
- intros; apply trans_equal with (Zgcd [b] [a]).
+ intros; transitivity (Z.gcd [b] [a]).
    apply spec_gcd_gt; auto with zarith.
  apply Zis_gcd_gcd; auto with zarith.
- apply Zgcd_is_pos.
+ apply Z.gcd_nonneg.
  apply Zis_gcd_sym; apply Zgcd_is_gcd.
  intros; apply spec_gcd_gt; auto with zarith.
  Qed.
@@ -1017,22 +1010,22 @@ Module Make (W0:CyclicType) <: NType.
  exact (ZnZ.spec_is_even x).
  Qed.
 
- Theorem spec_even: forall x, even x = Zeven_bool [x].
+ Theorem spec_even: forall x, even x = Z.even [x].
  Proof.
  intros x. assert (H := spec_even_aux x). symmetry.
- rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
- destruct (even x); rewrite H, ?Zplus_0_r.
+ rewrite (Z.div_mod [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Z.add_0_r.
  rewrite Zeven_bool_iff. apply Zeven_2p.
  apply not_true_is_false. rewrite Zeven_bool_iff.
  apply Zodd_not_Zeven. apply Zodd_2p_plus_1.
  Qed.
 
- Theorem spec_odd: forall x, odd x = Zodd_bool [x].
+ Theorem spec_odd: forall x, odd x = Z.odd [x].
  Proof.
  intros x. unfold odd.
  assert (H := spec_even_aux x). symmetry.
- rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
- destruct (even x); rewrite H, ?Zplus_0_r; simpl negb.
+ rewrite (Z.div_mod [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Z.add_0_r; simpl negb.
  apply not_true_is_false. rewrite Zodd_bool_iff.
  apply Zeven_not_Zodd. apply Zeven_2p.
  apply Zodd_bool_iff. apply Zodd_2p_plus_1.
@@ -1041,27 +1034,21 @@ Module Make (W0:CyclicType) <: NType.
  (** * Conversion *)
 
  Definition pheight p :=
-   Peano.pred (nat_of_P (get_height (ZnZ.digits (dom_op 0)) (plength p))).
+   Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))).
 
  Theorem pheight_correct: forall p,
-    Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z_of_nat (pheight p))).
+    Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))).
  Proof.
  intros p; unfold pheight.
- assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1).
-  intros x.
-  assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith.
-    rewrite <- inj_S.
-    rewrite <- (fun x => S_pred x 0); auto with zarith.
-    rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto.
-    apply lt_le_trans with 1%nat; auto with zarith.
-    exact (le_Pmult_nat x 1).
-  rewrite F1; clear F1.
+ rewrite Nat2Z.inj_pred by apply Pos2Nat.is_pos.
+ rewrite positive_nat_Z.
+ rewrite <- Z.sub_1_r.
  assert (F2:= (get_height_correct (ZnZ.digits (dom_op 0)) (plength p))).
- apply Zlt_le_trans with (Zpos (Psucc p)).
-   rewrite Zpos_succ_morphism; auto with zarith.
-  apply Zle_trans with (1 := plength_pred_correct (Psucc p)).
- rewrite Ppred_succ.
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.lt_le_trans with (Zpos (Pos.succ p)).
+   rewrite Pos2Z.inj_succ; auto with zarith.
+  apply Z.le_trans with (1 := plength_pred_correct (Pos.succ p)).
+ rewrite Pos.pred_succ.
+ apply Z.pow_le_mono_r; auto with zarith.
  Qed.
 
  Definition of_pos (x:positive) : t  :=
@@ -1076,8 +1063,8 @@ Module Make (W0:CyclicType) <: NType.
  simpl.
  apply ZnZ.of_pos_correct.
  unfold base.
- apply Zlt_le_trans with (1 := pheight_correct x).
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.lt_le_trans with (1 := pheight_correct x).
+ apply Z.pow_le_mono_r; auto with zarith.
  rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith.
  Qed.
 
@@ -1088,7 +1075,7 @@ Module Make (W0:CyclicType) <: NType.
   end.
 
  Theorem spec_of_N: forall x,
-   [of_N x] = Z_of_N x.
+   [of_N x] = Z.of_N x.
  Proof.
  intros x; case x.
   simpl of_N. exact spec_0.
@@ -1122,7 +1109,7 @@ Module Make (W0:CyclicType) <: NType.
   intros. apply Zdiv_unique with 0; auto with zarith.
   change 2 with (2^1) at 2.
   rewrite <- Zpower_exp; auto with zarith.
-  rewrite Zplus_0_r. f_equal. auto with zarith.
+  rewrite Z.add_0_r. f_equal. auto with zarith.
  Qed.
 
  Theorem spec_head0: forall x, 0 < [x] ->
@@ -1212,9 +1199,9 @@ Module Make (W0:CyclicType) <: NType.
  set (d := ZnZ.digits (dom_op n)) in *; clearbody d.
  destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso.
  assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h).
-  apply Zmult_le_compat; auto with zarith.
-  apply Zpower_le_monotone2; auto with zarith.
- rewrite Zmult_comm in H0. auto with zarith.
+  apply Z.mul_le_mono_nonneg; auto with zarith.
+  apply Z.pow_le_mono_r; auto with zarith.
+ rewrite Z.mul_comm in H0. auto with zarith.
  Qed.
 
  Lemma spec_log2_pos : forall x, [x]<>0 ->
@@ -1232,13 +1219,13 @@ Module Make (W0:CyclicType) <: NType.
  assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))).
  assert (H3 := head0_zdigits n x).
  rewrite Zmod_small by auto with zarith.
+ rewrite Z.sub_simpl_r.
  rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x))));
   auto with zarith.
  rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x))));
   auto with zarith.
  rewrite <- 2 Zpower_exp; auto with zarith.
- rewrite Z.add_sub_assoc, Zplus_minus.
- rewrite Z.sub_simpl_r, Zplus_minus.
+ rewrite !Z.add_sub_assoc, !Z.add_simpl_l.
  rewrite ZnZ.spec_zdigits.
  rewrite pow2_pos_minus_1 by (red; auto).
  apply ZnZ.spec_head0; auto with zarith.
@@ -1294,12 +1281,12 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
    intros x y z HH HH1 HH2.
    split; auto with zarith.
-   apply Zle_lt_trans with (2 := HH2); auto with zarith.
+   apply Z.le_lt_trans with (2 := HH2); auto with zarith.
    apply Zdiv_le_upper_bound; auto with zarith.
    pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.
-   apply Zmult_le_compat_l; auto.
-   apply Zpower_le_monotone2; auto with zarith.
-   rewrite Zpower_0_r; ring.
+   apply Z.mul_le_mono_nonneg_l; auto.
+   apply Z.pow_le_mono_r; auto with zarith.
+   rewrite Z.pow_0_r; ring.
  Qed.
 
  Theorem spec_shiftr_pow2 : forall x n,
@@ -1315,7 +1302,7 @@ Module Make (W0:CyclicType) <: NType.
   rewrite spec_reduce.
   rewrite ZnZ.spec_zdigits in H.
   rewrite ZnZ.spec_add_mul_div by auto with zarith.
-  rewrite ZnZ.spec_0, Zmult_0_l, Zplus_0_l.
+  rewrite ZnZ.spec_0, Z.mul_0_l, Z.add_0_l.
   rewrite Zmod_small.
   f_equal. f_equal. auto with zarith.
   split. auto with zarith.
@@ -1324,8 +1311,8 @@ Module Make (W0:CyclicType) <: NType.
   rewrite ZnZ.spec_0. symmetry.
   apply Zdiv_small.
   split; auto with zarith.
-  apply Zlt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith.
-  unfold base. apply Zpower_le_monotone2; auto with zarith.
+  apply Z.lt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith.
+  unfold base. apply Z.pow_le_mono_r; auto with zarith.
   rewrite ZnZ.spec_zdigits in H.
   generalize (ZnZ.spec_to_Z d); auto with zarith.
  Qed.
@@ -1370,21 +1357,21 @@ Module Make (W0:CyclicType) <: NType.
  destruct (ZnZ.spec_to_Z x).
  destruct (ZnZ.spec_to_Z p).
  rewrite ZnZ.spec_add_mul_div by (omega with *).
- rewrite ZnZ.spec_0, Zdiv_0_l, Zplus_0_r.
+ rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r.
  apply Zmod_small. unfold base.
  split; auto with zarith.
- rewrite Zmult_comm.
- apply Zlt_le_trans with (2^(ZnZ.to_Z p + K)).
+ rewrite Z.mul_comm.
+ apply Z.lt_le_trans with (2^(ZnZ.to_Z p + K)).
  rewrite Zpower_exp; auto with zarith.
- apply Zmult_lt_compat_l; auto with zarith.
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.mul_lt_mono_pos_l; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
  Qed.
 
  Theorem spec_unsafe_shiftl: forall x p,
   [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p].
  Proof.
  intros.
- destruct (Z_eq_dec [x] 0) as [EQ|NEQ].
+ destruct (Z.eq_dec [x] 0) as [EQ|NEQ].
  (* [x] = 0 *)
  apply spec_unsafe_shiftl_aux with 0; auto with zarith.
  now rewrite EQ.
@@ -1421,7 +1408,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros x. rewrite ! digits_level, double_size_level.
  rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower,
-         inj_S, Zpower_Zsucc; auto with zarith.
+         Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
  ring.
  Qed.
 
@@ -1438,46 +1425,47 @@ Module Make (W0:CyclicType) <: NType.
  assert (F1:= spec_pos (head0 x)).
  assert (F2: 0 < Zpos (digits x)).
    red; auto.
- case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH.
+ assert (HH := spec_pos x). Z.le_elim HH.
  generalize HH; rewrite <- (spec_double_size x); intros HH1.
  case (spec_head0 x HH); intros _ HH2.
  case (spec_head0 _ HH1).
  rewrite (spec_double_size x); rewrite (spec_double_size_digits x).
  intros HH3 _.
- case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4.
+ case (Z.le_gt_cases ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4.
  absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto.
- apply Zle_not_lt.
- apply Zmult_le_compat_r; auto with zarith.
- apply Zpower_le_monotone2; auto; auto with zarith.
+ apply Z.le_ngt.
+ apply Z.mul_le_mono_nonneg_r; auto with zarith.
+ apply Z.pow_le_mono_r; auto; auto with zarith.
  assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).
-   case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5.
-   apply Zmult_le_reg_r with (2 ^ 1); auto with zarith.
-   rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith.
-   assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp].
-   apply Zle_trans with (2 := Zlt_le_weak _ _ HH2).
-   apply Zmult_le_compat_l; auto with zarith.
-   rewrite Zpower_1_r; auto with zarith.
-   apply Zpower_le_monotone2; auto with zarith.
-   case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.
-   absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith.
-   rewrite <- HH5; rewrite Zmult_1_r.
-   apply Zpower_le_monotone2; auto with zarith.
- rewrite (Zmult_comm 2).
- rewrite Zpower_mult; auto with zarith.
- rewrite Zpower_2.
- apply Zlt_le_trans with (2 := HH3).
- rewrite <- Zmult_assoc.
+ { apply Z.le_succ_l in HH. change (1 <= [x]) in HH.
+   Z.le_elim HH.
+   - apply Z.mul_le_mono_pos_r with (2 ^ 1); auto with zarith.
+     rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith.
+     rewrite Z.sub_add.
+     apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2).
+     apply Z.mul_le_mono_nonneg_l; auto with zarith.
+     rewrite Z.pow_1_r; auto with zarith.
+   - apply Z.pow_le_mono_r; auto with zarith.
+     case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.
+     absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith.
+     rewrite <- HH; rewrite Z.mul_1_r.
+     apply Z.pow_le_mono_r; auto with zarith. }
+ rewrite (Z.mul_comm 2).
+ rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r.
+ apply Z.lt_le_trans with (2 := HH3).
+ rewrite <- Z.mul_assoc.
  replace (2 * Zpos (digits x) - 1) with
    ((Zpos (digits x) - 1) + (Zpos (digits x))).
  rewrite Zpower_exp; auto with zarith.
  apply Zmult_lt_compat2; auto with zarith.
  split; auto with zarith.
- apply Zmult_lt_0_compat; auto with zarith.
- rewrite Zpos_xO; ring.
- apply Zlt_le_weak; auto.
+ apply Z.mul_pos_pos; auto with zarith.
+ rewrite Pos2Z.inj_xO; ring.
+ apply Z.lt_le_incl; auto.
  repeat rewrite spec_head00; auto.
  rewrite spec_double_size_digits.
- rewrite Zpos_xO; auto with zarith.
+ rewrite Pos2Z.inj_xO; auto with zarith.
  rewrite spec_double_size; auto.
  Qed.
 
@@ -1485,24 +1473,26 @@ Module Make (W0:CyclicType) <: NType.
    forall x, 0 < [head0 (double_size x)].
  Proof.
  intros x.
- assert (F: 0 < Zpos (digits x)).
-  red; auto.
- case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0.
- case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1.
-   apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.
- case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3.
+ assert (F := Pos2Z.is_pos (digits x)).
+ assert (F0 := spec_pos (head0 (double_size x))).
+ Z.le_elim F0; auto.
+ assert (F1 := spec_pos (head0 x)).
+ Z.le_elim F1.
+  apply Z.lt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.
+ assert (F3 := spec_pos x).
+ Z.le_elim F3.
  generalize F3; rewrite <- (spec_double_size x); intros F4.
  absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).
-   apply Zle_not_lt.
-   apply Zpower_le_monotone2; auto with zarith.
-   rewrite Zpos_xO; auto with zarith.
+ { apply Z.le_ngt.
+   apply Z.pow_le_mono_r; auto with zarith.
+   rewrite Pos2Z.inj_xO; auto with zarith. }
  case (spec_head0 x F3).
- rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH.
- apply Zle_lt_trans with (2 := HH).
+ rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH.
+ apply Z.le_lt_trans with (2 := HH).
  case (spec_head0 _ F4).
  rewrite (spec_double_size x); rewrite (spec_double_size_digits x).
- rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto.
- generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith.
+ rewrite <- F0; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto.
+ generalize F1; rewrite (spec_head00 _ (eq_sym F3)); auto with zarith.
  Qed.
 
  (** Finally we iterate [double_size] enough before [unsafe_shiftl]
@@ -1521,14 +1511,14 @@ Module Make (W0:CyclicType) <: NType.
       [shiftl_aux_body cont x n] = [x] * 2 ^ [n].
  Proof.
  intros n x p cont H1 H2; unfold shiftl_aux_body.
- rewrite spec_compare; case Zcompare_spec; intros H.
+ rewrite spec_compare; case Z.compare_spec; intros H.
   apply spec_unsafe_shiftl; auto with zarith.
   apply spec_unsafe_shiftl; auto with zarith.
  rewrite H2.
  rewrite spec_double_size; auto.
- rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith.
- apply Zle_trans with (2 := spec_double_size_head0 x).
- rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith.
+ rewrite Z.add_comm; rewrite Zpower_exp; auto with zarith.
+ apply Z.le_trans with (2 := spec_double_size_head0 x).
+ rewrite Z.pow_1_r; apply Z.mul_le_mono_nonneg_l; auto with zarith.
  Qed.
 
  Fixpoint shiftl_aux p cont x n :=
@@ -1550,27 +1540,27 @@ Module Make (W0:CyclicType) <: NType.
  apply spec_shiftl_aux_body with (q); auto.
  intros x1 H3; apply Hrec with (q + 1)%positive; auto.
  intros x2 H4; apply Hrec with (p + q + 1)%positive; auto.
- rewrite <- Pplus_assoc.
- rewrite Zpos_plus_distr; auto.
+ rewrite <- Pos.add_assoc.
+ rewrite Pos2Z.inj_add; auto.
  intros x3 H5; apply H2.
- rewrite Zpos_xI.
+ rewrite Pos2Z.inj_xI.
  replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));
    auto.
- repeat rewrite Zpos_plus_distr; ring.
+ rewrite !Pos2Z.inj_add; ring.
  intros p Hrec q n x cont H1 H2.
  apply spec_shiftl_aux_body with (q); auto.
  intros x1 H3; apply Hrec with (q); auto.
- apply Zle_trans with (2 := H3); auto with zarith.
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.le_trans with (2 := H3); auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
  intros x2 H4; apply Hrec with (p + q)%positive; auto.
  intros x3 H5; apply H2.
- rewrite (Zpos_xO p).
+ rewrite (Pos2Z.inj_xO p).
  replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));
    auto.
- repeat rewrite Zpos_plus_distr; ring.
+ rewrite Pos2Z.inj_add; ring.
  intros q n x cont H1 H2.
  apply spec_shiftl_aux_body with (q); auto.
- rewrite Zplus_comm; auto.
+ rewrite Z.add_comm; auto.
  Qed.
 
  Definition shiftl x n :=
@@ -1582,25 +1572,25 @@ Module Make (W0:CyclicType) <: NType.
    [shiftl x n] = [x] * 2 ^ [n].
  Proof.
  intros x n; unfold shiftl, shiftl_aux_body.
- rewrite spec_compare; case Zcompare_spec; intros H.
+ rewrite spec_compare; case Z.compare_spec; intros H.
   apply spec_unsafe_shiftl; auto with zarith.
   apply spec_unsafe_shiftl; auto with zarith.
  rewrite <- (spec_double_size x).
- rewrite spec_compare; case Zcompare_spec; intros H1.
+ rewrite spec_compare; case Z.compare_spec; intros H1.
   apply spec_unsafe_shiftl; auto with zarith.
   apply spec_unsafe_shiftl; auto with zarith.
  rewrite <- (spec_double_size (double_size x)).
  apply spec_shiftl_aux with 1%positive.
- apply Zle_trans with (2 := spec_double_size_head0 (double_size x)).
+ apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)).
  replace (2 ^ 1) with (2 * 1).
- apply Zmult_le_compat_l; auto with zarith.
+ apply Z.mul_le_mono_nonneg_l; auto with zarith.
  generalize (spec_double_size_head0_pos x); auto with zarith.
- rewrite Zpower_1_r; ring.
+ rewrite Z.pow_1_r; ring.
  intros x1 H2; apply spec_unsafe_shiftl.
- apply Zle_trans with (2 := H2).
- apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith.
+ apply Z.le_trans with (2 := H2).
+ apply Z.le_trans with (2 ^ Zpos (digits n)); auto with zarith.
  case (spec_digits n); auto with zarith.
- apply Zpower_le_monotone2; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
  Qed.
 
  Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 59d440c3..278cc8bf 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -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        *)
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 4717d0b2..5bde1008 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.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        *)
@@ -32,7 +32,7 @@ Proof.
  transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
  rewrite <- IHn. auto.
  rewrite Z.mul_assoc.
- rewrite inj_S.
+ rewrite Nat2Z.inj_succ.
  rewrite <- Z.pow_succ_r; auto with zarith.
 Qed.
 
@@ -41,39 +41,39 @@ Qed.
 Fixpoint plength (p: positive) : positive :=
   match p with
     xH => xH
-  | xO p1 => Psucc (plength p1)
-  | xI p1 => Psucc (plength p1)
+  | xO p1 => Pos.succ (plength p1)
+  | xI p1 => Pos.succ (plength p1)
   end.
 
 Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
-assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
-intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
+assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z).
+intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z.
 rewrite Zpower_exp; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
 intros p; elim p; simpl plength; auto.
-intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
+intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI.
 assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
-intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
+intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1).
 assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
 Qed.
 
-Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
-intros p; case (Psucc_pred p); intros H1.
+Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z.
+intros p; case (Pos.succ_pred_or p); intros H1.
 subst; simpl plength.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
 pattern p at 1; rewrite <- H1.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
-generalize (plength_correct (Ppred p)); auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
+generalize (plength_correct (Pos.pred p)); auto with zarith.
 Qed.
 
 Definition Pdiv p q :=
-  match Zdiv (Zpos p) (Zpos q) with
+  match Z.div (Zpos p) (Zpos q) with
     Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
                  Z0 => q1
-               | _ => (Psucc q1)
+               | _ => (Pos.succ q1)
                end
   |  _ => xH
   end.
@@ -85,20 +85,20 @@ unfold Pdiv.
 assert (H1: Zpos q > 0); auto with zarith.
 assert (H1b: Zpos p >= 0); auto with zarith.
 generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b).
-generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv.
-  intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl.
+generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Z.div.
+  intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl.
 case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
 intros q1 H2.
 replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
   2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
 generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2;
-  case Zmod.
+  case Z.modulo.
   intros HH _; rewrite HH; auto with zarith.
-  intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
-  unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith.
+  intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ.
+  unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith.
   intros r1 _ (HH,_); case HH; auto.
 intros q1 HH; rewrite HH.
-unfold Zge; simpl Zcompare; intros HH1; case HH1; auto.
+unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto.
 Qed.
 
 Definition is_one p := match p with xH => true | _ => false end.
@@ -109,7 +109,7 @@ Qed.
 
 Definition get_height digits p :=
   let r := Pdiv p digits in
-   if is_one r then xH else Psucc (plength (Ppred r)).
+   if is_one r then xH else Pos.succ (plength (Pos.pred r)).
 
 Theorem get_height_correct:
   forall digits N,
@@ -119,13 +119,13 @@ unfold get_height.
 assert (H1 := Pdiv_le N digits).
 case_eq (is_one (Pdiv N digits)); intros H2.
 rewrite (is_one_one _ H2) in H1.
-rewrite Zmult_1_r in H1.
-change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto.
+rewrite Z.mul_1_r in H1.
+change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto.
 clear H2.
-apply Zle_trans with (1 := H1).
-apply Zmult_le_compat_l; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc.
-rewrite Zplus_comm; rewrite Zminus_plus.
+apply Z.le_trans with (1 := H1).
+apply Z.mul_le_mono_nonneg_l; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ.
+rewrite Z.add_comm; rewrite Z.add_simpl_l.
 apply plength_pred_correct.
 Qed.
 
@@ -152,18 +152,18 @@ Open Scope nat_scope.
 
 Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
   match n return  (n + S m = S (n + m))%nat with
-  | 0 => refl_equal (S m)
+  | 0 => eq_refl (S m)
   | S n1 =>
       let v := S (S n1 + m) in
-      eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
+      eq_ind_r (fun n => S n = v) (eq_refl v) (plusnS n1 m)
   end.
 
 Fixpoint plusn0 n : n + 0 = n :=
   match n return (n + 0 = n) with
-  | 0 => refl_equal 0
+  | 0 => eq_refl 0
   | S n1 =>
       let v := S n1 in
-      eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
+      eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1)
   end.
 
  Fixpoint diff (m n: nat) {struct m}: nat * nat :=
@@ -177,8 +177,8 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
   match m return fst (diff m n) + n = max m n with
   | 0 =>
       match n return (n = max 0 n) with
-      | 0 => refl_equal _
-      | S n0 => refl_equal _
+      | 0 => eq_refl _
+      | S n0 => eq_refl _
       end
   | S m1 =>
       match n return (fst (diff (S m1) n) + n = max (S m1) n)
@@ -188,7 +188,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
           let v := fst (diff m1 n1) + n1 in
           let v1 := fst (diff m1 n1) + S n1 in
           eq_ind v (fun n => v1 = S n)
-            (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
+            (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _))
             _ (diff_l _ _)
       end
   end.
@@ -197,17 +197,17 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
   match m return (snd (diff m n) + m = max m n) with
   | 0 =>
       match n return (snd (diff 0 n) + 0 = max 0 n) with
-      | 0 => refl_equal _
+      | 0 => eq_refl _
       | S _ => plusn0 _
       end
   | S m =>
       match n return (snd (diff (S m) n) + S m = max (S m) n) with
-      | 0 => refl_equal (snd (diff (S m) 0) + S m)
+      | 0 => eq_refl (snd (diff (S m) 0) + S m)
       | S n1 =>
           let v := S (max m n1) in
           eq_ind_r (fun n => n = v)
             (eq_ind_r (fun n => S n = v)
-               (refl_equal v) (diff_r _ _)) (plusnS _ _)
+               (eq_refl v) (diff_r _ _)) (plusnS _ _)
       end
   end.
 
@@ -216,7 +216,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
  Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
      (word w (S n)) :=
  match H in (_ = y) return (word w (S y)) with
- | refl_equal => x
+ | eq_refl => x
  end.
 
 Variable m: nat.
@@ -314,7 +314,7 @@ Section CompareRec.
  Lemma base_xO: forall n, base (xO n) = (base n)^2.
  Proof.
  intros n1; unfold base.
- rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
+ rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith.
  Qed.
 
  Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
@@ -332,13 +332,13 @@ Section CompareRec.
   rewrite 2 Hrec.
   simpl double_to_Z.
   set (wB := DoubleBase.double_wB wm_base n).
-  case Zcompare_spec; intros Cmp.
+  case Z.compare_spec; intros Cmp.
   rewrite <- Cmp. reflexivity.
-  symmetry. apply Zgt_lt, Zlt_gt. (* ;-) *)
+  symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *)
   assert (0 < wB).
    unfold wB, DoubleBase.double_wB, base; auto with zarith.
-  change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith.
-  apply Zmult_lt_0_compat; auto with zarith.
+  change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith.
+  apply Z.mul_pos_pos; auto with zarith.
   case (double_to_Z_pos n xl); auto with zarith.
   case (double_to_Z_pos n xh); intros; exfalso; omega.
   Qed.
@@ -358,9 +358,9 @@ Section CompareRec.
   end.
 
  Variable spec_compare: forall x y,
-   compare x y = Zcompare (w_to_Z x) (w_to_Z y).
+   compare x y = Z.compare (w_to_Z x) (w_to_Z y).
  Variable spec_compare_m: forall x y,
-   compare_m x y = Zcompare (wm_to_Z x) (w_to_Z y).
+   compare_m x y = Z.compare (wm_to_Z x) (w_to_Z y).
  Variable wm_base_lt: forall x,
    0 <= w_to_Z x < base (wm_base).
 
@@ -369,35 +369,35 @@ Section CompareRec.
  Proof.
  intros n x; elim n; simpl; auto; clear n.
  intros n (H0, H); split; auto.
- apply Zlt_le_trans with (1:= H).
+ apply Z.lt_le_trans with (1:= H).
  unfold double_wB, DoubleBase.double_wB; simpl.
  rewrite Pshiftl_nat_S, base_xO.
  set (u := base (Pos.shiftl_nat wm_base n)).
  assert (0 < u).
   unfold u, base; auto with zarith.
  replace (u^2) with (u * u); simpl; auto with zarith.
- apply Zle_trans with (1 * u); auto with zarith.
- unfold Zpower_pos; simpl; ring.
+ apply Z.le_trans with (1 * u); auto with zarith.
+ unfold Z.pow_pos; simpl; ring.
  Qed.
 
 
  Lemma spec_compare_mn_1: forall n x y,
-   compare_mn_1 n x y = Zcompare (double_to_Z n x) (w_to_Z y).
+   compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y).
  Proof.
  intros n; elim n; simpl; auto; clear n.
  intros n Hrec x; case x; clear x; auto.
  intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity.
  intros xh xl y; simpl;
- rewrite spec_compare0_mn, Hrec. case Zcompare_spec.
+ rewrite spec_compare0_mn, Hrec. case Z.compare_spec.
  intros H1b.
- rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto.
- symmetry. apply Zlt_gt.
+ rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto.
+ symmetry. apply Z.lt_gt.
  case (double_wB_lt n y); intros _ H0.
- apply Zlt_le_trans with (1:= H0).
+ apply Z.lt_le_trans with (1:= H0).
  fold double_wB.
  case (double_to_Z_pos n xl); intros H1 H2.
- apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith.
- apply Zle_trans with (1 * double_wB n); auto with zarith.
+ apply Z.le_trans with (double_to_Z n xh * double_wB n); auto with zarith.
+ apply Z.le_trans with (1 * double_wB n); auto with zarith.
  case (double_to_Z_pos n xh); intros; exfalso; omega.
  Qed.
 
@@ -440,8 +440,8 @@ End AddS.
  Proof.
  intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
    intros y; case y; clear y; intros y1 H || intros H; simpl length_pos;
-   try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
-   try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
+   try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1));
+   try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1));
    try (inversion H; fail);
    try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith);
    assert (0 < Zpos y1); auto with zarith; red; auto.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 43ca67dd..3150c561 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.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        *)
@@ -31,8 +31,8 @@ Time Eval vm_compute in (log 500000). (* 11 sec *)
 Fixpoint binposlog (p : positive) : N :=
 match p with
 | xH => 0
-| xO p' => Nsucc (binposlog p')
-| xI p' => Nsucc (binposlog p')
+| xO p' => N.succ (binposlog p')
+| xI p' => N.succ (binposlog p')
 end.
 
 Definition binlog (n : N) : N :=
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index d5df6329..a510b3ae 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.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        *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index aaf44ca6..0b8bded0 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.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        *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 2c7884ac..37d5db10 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.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        *)
@@ -318,7 +318,7 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
 Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b).
 Proof.
-intros a b. zify. intros. apply Z_div_mod_eq_full; auto.
+intros a b. zify. intros. apply Z.div_mod; auto.
 Qed.
 
 Theorem mod_bound_pos : forall a b, 0<=a -> 0<b ->
@@ -444,7 +444,7 @@ Qed.
 (** Recursion *)
 
 Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) :=
-  Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n).
+  N.peano_rect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n).
 Arguments recursion [A] a f n.
 
 Instance recursion_wd (A : Type) (Aeq : relation A) :
@@ -457,7 +457,7 @@ unfold NN.to_N.
 rewrite <- Exx'; clear x' Exx'.
 induction (Z.to_N [x]) using N.peano_ind.
 simpl; auto.
-rewrite 2 Nrect_step. now apply Eff'.
+rewrite 2 N.peano_rect_succ. now apply Eff'.
 Qed.
 
 Theorem recursion_0 :
@@ -474,7 +474,7 @@ Proof.
 unfold eq, recursion; intros A Aeq a f EAaa f_wd n.
 replace (to_N (succ n)) with (N.succ (to_N n)) by
  (zify; now rewrite <- Z2N.inj_succ by apply spec_pos).
-rewrite Nrect_step.
+rewrite N.peano_rect_succ.
 apply f_wd; auto.
 zify. now rewrite Z2N.id by apply spec_pos.
 fold (recursion a f n). apply recursion_wd; auto. red; auto.