Imported Upstream version 8.4dfsgupstream/8.4dfsg

10 files changed, 510 insertions, 644 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 30e35f50..5b1e83e6 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.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        *)
@@ -76,7 +76,7 @@ Defined.
 
 (** Discrimination principle *)
 
-Definition discr n : { p:positive | n = Npos p } + { n = N0 }.
+Definition discr n : { p:positive | n = pos p } + { n = 0 }.
 Proof.
  destruct n; auto.
  left; exists p; auto.
@@ -87,12 +87,12 @@ Defined.
 Definition binary_rect (P:N -> Type) (f0 : P 0)
   (f2 : forall n, P n -> P (double n))
   (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n :=
- let P' p := P (Npos p) in
- let f2' p := f2 (Npos p) in
- let fS2' p := fS2 (Npos p) in
+ let P' p := P (pos p) in
+ let f2' p := f2 (pos p) in
+ let fS2' p := fS2 (pos p) in
  match n with
  | 0 => f0
- | Npos p => positive_rect P' fS2' f2' (fS2 0 f0) p
+ | pos p => positive_rect P' fS2' f2' (fS2 0 f0) p
  end.
 
 Definition binary_rec (P:N -> Set) := binary_rect P.
@@ -103,11 +103,11 @@ Definition binary_ind (P:N -> Prop) := binary_rect P.
 Definition peano_rect
   (P : N -> Type) (f0 : P 0)
     (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
-let P' p := P (Npos p) in
-let f' p := f (Npos p) in
+let P' p := P (pos p) in
+let f' p := f (pos p) in
 match n with
 | 0 => f0
-| Npos p => Pos.peano_rect P' (f 0 f0) f' p
+| pos p => Pos.peano_rect P' (f 0 f0) f' p
 end.
 
 Theorem peano_rect_base P a f : peano_rect P a f 0 = a.
@@ -140,12 +140,12 @@ Qed.
 
 (** Properties of mixed successor and predecessor. *)
 
-Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p).
+Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).
 Proof.
  now destruct p.
 Qed.
 
-Lemma succ_pos_spec n : Npos (succ_pos n) = succ n.
+Lemma succ_pos_spec n : pos (succ_pos n) = succ n.
 Proof.
  now destruct n.
 Qed.
@@ -155,7 +155,7 @@ Proof.
  destruct n. trivial. apply Pos.pred_N_succ.
 Qed.
 
-Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p.
+Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.
 Proof.
  destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double.
 Qed.
@@ -472,7 +472,7 @@ Lemma log2_spec n : 0 < n ->
  2^(log2 n) <= n < 2^(succ (log2 n)).
 Proof.
  destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.
- apply (size_le (Npos p)).
+ apply (size_le (pos p)).
  apply Pos.size_gt.
  apply Pos.size_le.
  apply Pos.size_gt.
@@ -494,7 +494,7 @@ Proof.
  trivial.
  destruct p; simpl; split; try easy.
  intros (m,H). now destruct m.
- now exists (Npos p).
+ now exists (pos p).
  intros (m,H). now destruct m.
 Qed.
 
@@ -504,7 +504,7 @@ Proof.
  split. discriminate.
  intros (m,H). now destruct m.
  destruct p; simpl; split; try easy.
- now exists (Npos p).
+ now exists (pos p).
  intros (m,H). now destruct m.
  now exists 0.
 Qed.
@@ -512,19 +512,19 @@ Qed.
 (** Specification of the euclidean division *)
 
 Theorem pos_div_eucl_spec (a:positive)(b:N) :
-  let (q,r) := pos_div_eucl a b in Npos a = q * b + r.
+  let (q,r) := pos_div_eucl a b in pos a = q * b + r.
 Proof.
   induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.
   (* a~1 *)
   destruct pos_div_eucl as (q,r).
-  change (Npos a~1) with (succ_double (Npos a)).
+  change (pos a~1) with (succ_double (pos a)).
   rewrite IHa, succ_double_add, double_mul.
   case leb_spec; intros H; trivial.
   rewrite succ_double_mul, <- add_assoc. f_equal.
   now rewrite (add_comm b), sub_add.
   (* a~0 *)
   destruct pos_div_eucl as (q,r).
-  change (Npos a~0) with (double (Npos a)).
+  change (pos a~0) with (double (pos a)).
   rewrite IHa, double_add, double_mul.
   case leb_spec; intros H; trivial.
   rewrite succ_double_mul, <- add_assoc. f_equal.
@@ -537,7 +537,7 @@ Theorem div_eucl_spec a b :
  let (q,r) := div_eucl a b in a = b * q + r.
 Proof.
   destruct a as [|a], b as [|b]; unfold div_eucl; trivial.
-  generalize (pos_div_eucl_spec a (Npos b)).
+  generalize (pos_div_eucl_spec a (pos b)).
   destruct pos_div_eucl. now rewrite mul_comm.
 Qed.
 
@@ -664,7 +664,7 @@ Proof.
  destruct (Pos.gcd_greatest p q r) as (u,H).
  exists s. now inversion Hs.
  exists t. now inversion Ht.
- exists (Npos u). simpl; now f_equal.
+ exists (pos u). simpl; now f_equal.
 Qed.
 
 Lemma gcd_nonneg a b : 0 <= gcd a b.
@@ -862,7 +862,7 @@ Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
 Theorem bi_induction :
   forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
-    A N0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
+    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
 Proof.
 intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
 Qed.
@@ -893,11 +893,11 @@ Qed.
 
 (** Instantiation of generic properties of natural numbers *)
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+(** The Bind Scope prevents N to stay associated with abstract_scope.
+    (TODO FIX) *)
 
-(** Otherwise N stays associated with abstract_scope : (TODO FIX) *)
-Bind Scope N_scope with N.
+Include NProp. Bind Scope N_scope with N.
+Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1013,95 +1013,95 @@ Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope.
 
 (** Compatibility notations *)
 
-(*Notation N := N (only parsing).*) (*hidden by module N above *)
+(*Notation N := N (compat "8.3").*) (*hidden by module N above *)
 Notation N_rect := N_rect (only parsing).
 Notation N_rec := N_rec (only parsing).
 Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
-Notation Npos := Npos (only parsing).
-
-Notation Ndiscr := N.discr (only parsing).
-Notation Ndouble_plus_one := N.succ_double.
-Notation Ndouble := N.double (only parsing).
-Notation Nsucc := N.succ (only parsing).
-Notation Npred := N.pred (only parsing).
-Notation Nsucc_pos := N.succ_pos (only parsing).
-Notation Ppred_N := Pos.pred_N (only parsing).
-Notation Nplus := N.add (only parsing).
-Notation Nminus := N.sub (only parsing).
-Notation Nmult := N.mul (only parsing).
-Notation Neqb := N.eqb (only parsing).
-Notation Ncompare := N.compare (only parsing).
-Notation Nlt := N.lt (only parsing).
-Notation Ngt := N.gt (only parsing).
-Notation Nle := N.le (only parsing).
-Notation Nge := N.ge (only parsing).
-Notation Nmin := N.min (only parsing).
-Notation Nmax := N.max (only parsing).
-Notation Ndiv2 := N.div2 (only parsing).
-Notation Neven := N.even (only parsing).
-Notation Nodd := N.odd (only parsing).
-Notation Npow := N.pow (only parsing).
-Notation Nlog2 := N.log2 (only parsing).
-
-Notation nat_of_N := N.to_nat (only parsing).
-Notation N_of_nat := N.of_nat (only parsing).
-Notation N_eq_dec := N.eq_dec (only parsing).
-Notation Nrect := N.peano_rect (only parsing).
-Notation Nrect_base := N.peano_rect_base (only parsing).
-Notation Nrect_step := N.peano_rect_succ (only parsing).
-Notation Nind := N.peano_ind (only parsing).
-Notation Nrec := N.peano_rec (only parsing).
-Notation Nrec_base := N.peano_rec_base (only parsing).
-Notation Nrec_succ := N.peano_rec_succ (only parsing).
-
-Notation Npred_succ := N.pred_succ (only parsing).
-Notation Npred_minus := N.pred_sub (only parsing).
-Notation Nsucc_pred := N.succ_pred (only parsing).
-Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
-Notation Nsucc_pos_spec := N.succ_pos_spec (only parsing).
-Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
-Notation Nplus_0_l := N.add_0_l (only parsing).
-Notation Nplus_0_r := N.add_0_r (only parsing).
-Notation Nplus_comm := N.add_comm (only parsing).
-Notation Nplus_assoc := N.add_assoc (only parsing).
-Notation Nplus_succ := N.add_succ_l (only parsing).
-Notation Nsucc_0 := N.succ_0_discr (only parsing).
-Notation Nsucc_inj := N.succ_inj (only parsing).
-Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
-Notation Nminus_0_r := N.sub_0_r (only parsing).
-Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
-Notation Nmult_0_l := N.mul_0_l (only parsing).
-Notation Nmult_1_l := N.mul_1_l (only parsing).
-Notation Nmult_1_r := N.mul_1_r (only parsing).
-Notation Nmult_comm := N.mul_comm (only parsing).
-Notation Nmult_assoc := N.mul_assoc (only parsing).
-Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
-Notation Neqb_eq := N.eqb_eq (only parsing).
-Notation Nle_0 := N.le_0_l (only parsing).
-Notation Ncompare_refl := N.compare_refl (only parsing).
-Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
-Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
-Notation Nlt_irrefl := N.lt_irrefl (only parsing).
-Notation Nlt_trans := N.lt_trans (only parsing).
-Notation Nle_lteq := N.lt_eq_cases (only parsing).
-Notation Nlt_succ_r := N.lt_succ_r (only parsing).
-Notation Nle_trans := N.le_trans (only parsing).
-Notation Nle_succ_l := N.le_succ_l (only parsing).
-Notation Ncompare_spec := N.compare_spec (only parsing).
-Notation Ncompare_0 := N.compare_0_r (only parsing).
-Notation Ndouble_div2 := N.div2_double (only parsing).
-Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
-Notation Ndouble_inj := N.double_inj (only parsing).
-Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
-Notation Npow_0_r := N.pow_0_r (only parsing).
-Notation Npow_succ_r := N.pow_succ_r (only parsing).
-Notation Nlog2_spec := N.log2_spec (only parsing).
-Notation Nlog2_nonpos := N.log2_nonpos (only parsing).
-Notation Neven_spec := N.even_spec (only parsing).
-Notation Nodd_spec := N.odd_spec (only parsing).
-Notation Nlt_not_eq := N.lt_neq (only parsing).
-Notation Ngt_Nlt := N.gt_lt (only parsing).
+Notation Npos := N.pos (only parsing).
+
+Notation Ndiscr := N.discr (compat "8.3").
+Notation Ndouble_plus_one := N.succ_double (compat "8.3").
+Notation Ndouble := N.double (compat "8.3").
+Notation Nsucc := N.succ (compat "8.3").
+Notation Npred := N.pred (compat "8.3").
+Notation Nsucc_pos := N.succ_pos (compat "8.3").
+Notation Ppred_N := Pos.pred_N (compat "8.3").
+Notation Nplus := N.add (compat "8.3").
+Notation Nminus := N.sub (compat "8.3").
+Notation Nmult := N.mul (compat "8.3").
+Notation Neqb := N.eqb (compat "8.3").
+Notation Ncompare := N.compare (compat "8.3").
+Notation Nlt := N.lt (compat "8.3").
+Notation Ngt := N.gt (compat "8.3").
+Notation Nle := N.le (compat "8.3").
+Notation Nge := N.ge (compat "8.3").
+Notation Nmin := N.min (compat "8.3").
+Notation Nmax := N.max (compat "8.3").
+Notation Ndiv2 := N.div2 (compat "8.3").
+Notation Neven := N.even (compat "8.3").
+Notation Nodd := N.odd (compat "8.3").
+Notation Npow := N.pow (compat "8.3").
+Notation Nlog2 := N.log2 (compat "8.3").
+
+Notation nat_of_N := N.to_nat (compat "8.3").
+Notation N_of_nat := N.of_nat (compat "8.3").
+Notation N_eq_dec := N.eq_dec (compat "8.3").
+Notation Nrect := N.peano_rect (compat "8.3").
+Notation Nrect_base := N.peano_rect_base (compat "8.3").
+Notation Nrect_step := N.peano_rect_succ (compat "8.3").
+Notation Nind := N.peano_ind (compat "8.3").
+Notation Nrec := N.peano_rec (compat "8.3").
+Notation Nrec_base := N.peano_rec_base (compat "8.3").
+Notation Nrec_succ := N.peano_rec_succ (compat "8.3").
+
+Notation Npred_succ := N.pred_succ (compat "8.3").
+Notation Npred_minus := N.pred_sub (compat "8.3").
+Notation Nsucc_pred := N.succ_pred (compat "8.3").
+Notation Ppred_N_spec := N.pos_pred_spec (compat "8.3").
+Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.3").
+Notation Ppred_Nsucc := N.pos_pred_succ (compat "8.3").
+Notation Nplus_0_l := N.add_0_l (compat "8.3").
+Notation Nplus_0_r := N.add_0_r (compat "8.3").
+Notation Nplus_comm := N.add_comm (compat "8.3").
+Notation Nplus_assoc := N.add_assoc (compat "8.3").
+Notation Nplus_succ := N.add_succ_l (compat "8.3").
+Notation Nsucc_0 := N.succ_0_discr (compat "8.3").
+Notation Nsucc_inj := N.succ_inj (compat "8.3").
+Notation Nminus_N0_Nle := N.sub_0_le (compat "8.3").
+Notation Nminus_0_r := N.sub_0_r (compat "8.3").
+Notation Nminus_succ_r:= N.sub_succ_r (compat "8.3").
+Notation Nmult_0_l := N.mul_0_l (compat "8.3").
+Notation Nmult_1_l := N.mul_1_l (compat "8.3").
+Notation Nmult_1_r := N.mul_1_r (compat "8.3").
+Notation Nmult_comm := N.mul_comm (compat "8.3").
+Notation Nmult_assoc := N.mul_assoc (compat "8.3").
+Notation Nmult_plus_distr_r := N.mul_add_distr_r (compat "8.3").
+Notation Neqb_eq := N.eqb_eq (compat "8.3").
+Notation Nle_0 := N.le_0_l (compat "8.3").
+Notation Ncompare_refl := N.compare_refl (compat "8.3").
+Notation Ncompare_Eq_eq := N.compare_eq (compat "8.3").
+Notation Ncompare_eq_correct := N.compare_eq_iff (compat "8.3").
+Notation Nlt_irrefl := N.lt_irrefl (compat "8.3").
+Notation Nlt_trans := N.lt_trans (compat "8.3").
+Notation Nle_lteq := N.lt_eq_cases (compat "8.3").
+Notation Nlt_succ_r := N.lt_succ_r (compat "8.3").
+Notation Nle_trans := N.le_trans (compat "8.3").
+Notation Nle_succ_l := N.le_succ_l (compat "8.3").
+Notation Ncompare_spec := N.compare_spec (compat "8.3").
+Notation Ncompare_0 := N.compare_0_r (compat "8.3").
+Notation Ndouble_div2 := N.div2_double (compat "8.3").
+Notation Ndouble_plus_one_div2 := N.div2_succ_double (compat "8.3").
+Notation Ndouble_inj := N.double_inj (compat "8.3").
+Notation Ndouble_plus_one_inj := N.succ_double_inj (compat "8.3").
+Notation Npow_0_r := N.pow_0_r (compat "8.3").
+Notation Npow_succ_r := N.pow_succ_r (compat "8.3").
+Notation Nlog2_spec := N.log2_spec (compat "8.3").
+Notation Nlog2_nonpos := N.log2_nonpos (compat "8.3").
+Notation Neven_spec := N.even_spec (compat "8.3").
+Notation Nodd_spec := N.odd_spec (compat "8.3").
+Notation Nlt_not_eq := N.lt_neq (compat "8.3").
+Notation Ngt_Nlt := N.gt_lt (compat "8.3").
 
 (** More complex compatibility facts, expressed as lemmas
     (to preserve scopes for instance) *)
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index d7660422..08e1138f 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.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        *)
@@ -19,6 +19,10 @@ Module N.
 
 Definition t := N.
 
+(** ** Nicer name [N.pos] for contructor [Npos] *)
+
+Notation pos := Npos.
+
 (** ** Constants *)
 
 Definition zero := 0.
@@ -30,7 +34,7 @@ Definition two := 2.
 Definition succ_double x :=
   match x with
   | 0 => 1
-  | Npos p => Npos p~1
+  | pos p => pos p~1
   end.
 
 (** ** Operation [x -> 2*x] *)
@@ -38,7 +42,7 @@ Definition succ_double x :=
 Definition double n :=
   match n with
   | 0 => 0
-  | Npos p => Npos p~0
+  | pos p => pos p~0
   end.
 
 (** ** Successor *)
@@ -46,7 +50,7 @@ Definition double n :=
 Definition succ n :=
   match n with
   | 0 => 1
-  | Npos p => Npos (Pos.succ p)
+  | pos p => pos (Pos.succ p)
   end.
 
 (** ** Predecessor *)
@@ -54,15 +58,15 @@ Definition succ n :=
 Definition pred n :=
   match n with
   | 0 => 0
-  | Npos p => Pos.pred_N p
+  | pos p => Pos.pred_N p
   end.
 
 (** ** The successor of a [N] can be seen as a [positive] *)
 
 Definition succ_pos (n : N) : positive :=
  match n with
-   | N0 => 1%positive
-   | Npos p => Pos.succ p
+   | 0 => 1%positive
+   | pos p => Pos.succ p
  end.
 
 (** ** Addition *)
@@ -71,7 +75,7 @@ Definition add n m :=
   match n, m with
   | 0, _ => m
   | _, 0 => n
-  | Npos p, Npos q => Npos (p + q)
+  | pos p, pos q => pos (p + q)
   end.
 
 Infix "+" := add : N_scope.
@@ -82,9 +86,9 @@ Definition sub n m :=
 match n, m with
 | 0, _ => 0
 | n, 0 => n
-| Npos n', Npos m' =>
+| pos n', pos m' =>
   match Pos.sub_mask n' m' with
-  | IsPos p => Npos p
+  | IsPos p => pos p
   | _ => 0
   end
 end.
@@ -97,7 +101,7 @@ Definition mul n m :=
   match n, m with
   | 0, _ => 0
   | _, 0 => 0
-  | Npos p, Npos q => Npos (p * q)
+  | pos p, pos q => pos (p * q)
   end.
 
 Infix "*" := mul : N_scope.
@@ -107,23 +111,19 @@ Infix "*" := mul : N_scope.
 Definition compare n m :=
   match n, m with
   | 0, 0 => Eq
-  | 0, Npos m' => Lt
-  | Npos n', 0 => Gt
-  | Npos n', Npos m' => (n' ?= m')%positive
+  | 0, pos m' => Lt
+  | pos n', 0 => Gt
+  | pos n', pos m' => (n' ?= m')%positive
   end.
 
 Infix "?=" := compare (at level 70, no associativity) : N_scope.
 
 (** Boolean equality and comparison *)
 
-(** Nota: this [eqb] is not convertible with the generated [N_beq],
-    since the underlying [Pos.eqb] differs from [positive_beq]
-    (cf BinIntDef). *)
-
 Fixpoint eqb n m :=
   match n, m with
     | 0, 0 => true
-    | Npos p, Npos q => Pos.eqb p q
+    | pos p, pos q => Pos.eqb p q
     | _, _ => false
   end.
 
@@ -155,8 +155,8 @@ Definition div2 n :=
   match n with
   | 0 => 0
   | 1 => 0
-  | Npos (p~0) => Npos p
-  | Npos (p~1) => Npos p
+  | pos (p~0) => pos p
+  | pos (p~1) => pos p
   end.
 
 (** Parity *)
@@ -164,7 +164,7 @@ Definition div2 n :=
 Definition even n :=
   match n with
     | 0 => true
-    | Npos (xO _) => true
+    | pos (xO _) => true
     | _ => false
   end.
 
@@ -176,7 +176,7 @@ Definition pow n p :=
   match p, n with
     | 0, _ => 1
     | _, 0 => 0
-    | Npos p, Npos q => Npos (q^p)
+    | pos p, pos q => pos (q^p)
   end.
 
 Infix "^" := pow : N_scope.
@@ -186,7 +186,7 @@ Infix "^" := pow : N_scope.
 Definition square n :=
   match n with
     | 0 => 0
-    | Npos p => Npos (Pos.square p)
+    | pos p => pos (Pos.square p)
   end.
 
 (** Base-2 logarithm *)
@@ -195,8 +195,8 @@ Definition log2 n :=
  match n with
    | 0 => 0
    | 1 => 0
-   | Npos (p~0) => Npos (Pos.size p)
-   | Npos (p~1) => Npos (Pos.size p)
+   | pos (p~0) => pos (Pos.size p)
+   | pos (p~1) => pos (Pos.size p)
  end.
 
 (** How many digits in a number ?
@@ -206,13 +206,13 @@ Definition log2 n :=
 Definition size n :=
  match n with
   | 0 => 0
-  | Npos p => Npos (Pos.size p)
+  | pos p => pos (Pos.size p)
  end.
 
 Definition size_nat n :=
  match n with
   | 0 => O
-  | Npos p => Pos.size_nat p
+  | pos p => Pos.size_nat p
  end.
 
 (** Euclidean division *)
@@ -237,7 +237,7 @@ Definition div_eucl (a b:N) : N * N :=
   match a, b with
    | 0,  _ => (0, 0)
    | _, 0  => (0, a)
-   | Npos na, _ => pos_div_eucl na b
+   | pos na, _ => pos_div_eucl na b
   end.
 
 Definition div a b := fst (div_eucl a b).
@@ -252,7 +252,7 @@ Definition gcd a b :=
  match a, b with
   | 0, _ => b
   | _, 0 => a
-  | Npos p, Npos q => Npos (Pos.gcd p q)
+  | pos p, pos q => pos (Pos.gcd p q)
  end.
 
 (** Generalized Gcd, also computing rests of [a] and [b] after
@@ -262,9 +262,9 @@ Definition ggcd a b :=
  match a, b with
   | 0, _ => (b,(0,1))
   | _, 0 => (a,(1,0))
-  | Npos p, Npos q =>
+  | pos p, pos q =>
      let '(g,(aa,bb)) := Pos.ggcd p q in
-     (Npos g, (Npos aa, Npos bb))
+     (pos g, (pos aa, pos bb))
  end.
 
 (** Square root *)
@@ -272,17 +272,17 @@ Definition ggcd a b :=
 Definition sqrtrem n :=
  match n with
   | 0 => (0, 0)
-  | Npos p =>
+  | pos p =>
     match Pos.sqrtrem p with
-     | (s, IsPos r) => (Npos s, Npos r)
-     | (s, _) => (Npos s, 0)
+     | (s, IsPos r) => (pos s, pos r)
+     | (s, _) => (pos s, 0)
     end
  end.
 
 Definition sqrt n :=
  match n with
   | 0 => 0
-  | Npos p => Npos (Pos.sqrt p)
+  | pos p => pos (Pos.sqrt p)
  end.
 
 (** Operation over bits of a [N] number. *)
@@ -293,7 +293,7 @@ Definition lor n m :=
  match n, m with
    | 0, _ => m
    | _, 0 => n
-   | Npos p, Npos q => Npos (Pos.lor p q)
+   | pos p, pos q => pos (Pos.lor p q)
  end.
 
 (** Logical [and] *)
@@ -302,7 +302,7 @@ Definition land n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => 0
-  | Npos p, Npos q => Pos.land p q
+  | pos p, pos q => Pos.land p q
  end.
 
 (** Logical [diff] *)
@@ -311,7 +311,7 @@ Fixpoint ldiff n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => n
-  | Npos p, Npos q => Pos.ldiff p q
+  | pos p, pos q => Pos.ldiff p q
  end.
 
 (** [xor] *)
@@ -320,7 +320,7 @@ Definition lxor n m :=
   match n, m with
     | 0, _ => m
     | _, 0 => n
-    | Npos p, Npos q => Pos.lxor p q
+    | pos p, pos q => Pos.lxor p q
   end.
 
 (** Shifts *)
@@ -331,13 +331,13 @@ Definition shiftr_nat (a:N)(n:nat) := nat_iter n div2 a.
 Definition shiftl a n :=
   match a with
     | 0 => 0
-    | Npos a => Npos (Pos.shiftl a n)
+    | pos a => pos (Pos.shiftl a n)
   end.
 
 Definition shiftr a n :=
   match n with
     | 0 => a
-    | Npos p => Pos.iter p div2 a
+    | pos p => Pos.iter p div2 a
   end.
 
 (** Checking whether a particular bit is set or not *)
@@ -345,7 +345,7 @@ Definition shiftr a n :=
 Definition testbit_nat (a:N) :=
   match a with
     | 0 => fun _ => false
-    | Npos p => Pos.testbit_nat p
+    | pos p => Pos.testbit_nat p
   end.
 
 (** Same, but with index in N *)
@@ -353,7 +353,7 @@ Definition testbit_nat (a:N) :=
 Definition testbit a n :=
   match a with
     | 0 => false
-    | Npos p => Pos.testbit p n
+    | pos p => Pos.testbit p n
   end.
 
 (** Translation from [N] to [nat] and back. *)
@@ -361,13 +361,13 @@ Definition testbit a n :=
 Definition to_nat (a:N) :=
   match a with
     | 0 => O
-    | Npos p => Pos.to_nat p
+    | pos p => Pos.to_nat p
   end.
 
 Definition of_nat (n:nat) :=
   match n with
     | O => 0
-    | S n' => Npos (Pos.of_succ_nat n')
+    | S n' => pos (Pos.of_succ_nat n')
   end.
 
 (** Iteration of a function *)
@@ -375,7 +375,7 @@ Definition of_nat (n:nat) :=
 Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
   match n with
     | 0 => x
-    | Npos p => Pos.iter p f x
+    | pos p => Pos.iter p f x
   end.
 
 End N.
\ No newline at end of file
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 4a5f4ee1..d0664d37 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.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/NArith/Ndec.v b/theories/NArith/Ndec.v
index f2ee29cc..f8db7548 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.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        *)
@@ -15,315 +15,238 @@ Require Import Pnat.
 Require Import Nnat.
 Require Import Ndigits.
 
-(** A boolean equality over [N] *)
+Local Open Scope N_scope.
 
-Notation Peqb := Peqb (only parsing). (* Now in [BinPos] *)
-Notation Neqb := Neqb (only parsing). (* Now in [BinNat] *)
+(** Obsolete results about boolean comparisons over [N],
+    kept for compatibility with IntMap and SMC. *)
 
-Notation Peqb_correct := Peqb_refl (only parsing).
+Notation Peqb := Pos.eqb (compat "8.3").
+Notation Neqb := N.eqb (compat "8.3").
+Notation Peqb_correct := Pos.eqb_refl (compat "8.3").
+Notation Neqb_correct := N.eqb_refl (compat "8.3").
+Notation Neqb_comm := N.eqb_sym (compat "8.3").
 
-Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.
-Proof.
-  intros. now apply (Peqb_eq p p').
-Qed.
+Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'.
+Proof. now apply Pos.eqb_eq. Qed.
 
-Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pos.compare p p' = Eq.
-Proof.
-  intros. now rewrite Pos.compare_eq_iff, <- Peqb_eq.
-Qed.
-
-Lemma Pcompare_Peqb : forall p p', Pos.compare p p' = Eq -> Peqb p p' = true.
-Proof.
-  intros; now rewrite Peqb_eq, <- Pos.compare_eq_iff.
-Qed.
+Lemma Peqb_Pcompare p p' : Pos.eqb p p' = true -> Pos.compare p p' = Eq.
+Proof. now rewrite Pos.compare_eq_iff, <- Pos.eqb_eq. Qed.
 
-Lemma Neqb_correct : forall n, Neqb n n = true.
-Proof.
-  intros; now rewrite Neqb_eq.
-Qed.
+Lemma Pcompare_Peqb p p' : Pos.compare p p' = Eq -> Pos.eqb p p' = true.
+Proof. now rewrite Pos.eqb_eq, <- Pos.compare_eq_iff. Qed.
 
-Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq.
-Proof.
-  intros; now rewrite Ncompare_eq_correct, <- Neqb_eq.
-Qed.
+Lemma Neqb_Ncompare n n' : N.eqb n n' = true -> N.compare n n' = Eq.
+Proof. now rewrite N.compare_eq_iff, <- N.eqb_eq. Qed.
 
-Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true.
-Proof.
-  intros; now rewrite Neqb_eq, <- Ncompare_eq_correct.
-Qed.
+Lemma Ncompare_Neqb n n' : N.compare n n' = Eq -> N.eqb n n' = true.
+Proof. now rewrite N.eqb_eq, <- N.compare_eq_iff. Qed.
 
-Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'.
-Proof.
-  intros; now rewrite <- Neqb_eq.
-Qed.
+Lemma Neqb_complete n n' : N.eqb n n' = true -> n = n'.
+Proof. now apply N.eqb_eq. Qed.
 
-Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a.
+Lemma Nxor_eq_true n n' : N.lxor n n' = 0 -> N.eqb n n' = true.
 Proof.
-  intros; apply eq_true_iff_eq. rewrite 2 Neqb_eq; auto with *.
+  intro H. apply N.lxor_eq in H. subst. apply N.eqb_refl.
 Qed.
 
-Lemma Nxor_eq_true :
- forall a a', Nxor a a' = N0 -> Neqb a a' = true.
-Proof.
-  intros. rewrite (Nxor_eq a a' H). apply Neqb_correct.
-Qed.
+Ltac eqb2eq := rewrite <- ?not_true_iff_false in *; rewrite ?N.eqb_eq in *.
 
-Lemma Nxor_eq_false :
- forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false.
+Lemma Nxor_eq_false n n' p :
+  N.lxor n n' = N.pos p -> N.eqb n n' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete a a' H0) in H.
-  rewrite (Nxor_nilpotent a') in H. discriminate H.
-  trivial.
+  intros. eqb2eq. intro. subst. now rewrite N.lxor_nilpotent in *.
 Qed.
 
-Lemma Nodd_not_double :
- forall a,
-   Nodd a -> forall a0, Neqb (Ndouble a0) a = false.
+Lemma Nodd_not_double a :
+  Nodd a -> forall a0, N.eqb (N.double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H.
-  unfold Nodd in H.
-  rewrite (Ndouble_bit0 a0) in H. discriminate H.
-  trivial.
+  intros. eqb2eq. intros <-.
+  unfold Nodd in *. now rewrite Ndouble_bit0 in *.
 Qed.
 
-Lemma Nnot_div2_not_double :
- forall a a0,
-   Neqb (Ndiv2 a) a0 = false -> Neqb a (Ndouble a0) = false.
+Lemma Nnot_div2_not_double a a0 :
+  N.eqb (N.div2 a) a0 = false -> N.eqb a (N.double a0) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H. rewrite (Ndouble_div2 a0) in H.
-  rewrite (Neqb_correct a0) in H. discriminate H.
-  intro. rewrite Neqb_comm. assumption.
+  intros H. eqb2eq. contradict H. subst. apply N.div2_double.
 Qed.
 
-Lemma Neven_not_double_plus_one :
- forall a,
-   Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false.
+Lemma Neven_not_double_plus_one a :
+  Neven a -> forall a0, N.eqb (N.succ_double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H.
-  unfold Neven in H.
-  rewrite (Ndouble_plus_one_bit0 a0) in H.
-  discriminate H.
-  trivial.
+  intros. eqb2eq. intros <-.
+  unfold Neven in *. now rewrite Ndouble_plus_one_bit0 in *.
 Qed.
 
-Lemma Nnot_div2_not_double_plus_one :
- forall a a0,
-   Neqb (Ndiv2 a) a0 = false -> Neqb (Ndouble_plus_one a0) a = false.
+Lemma Nnot_div2_not_double_plus_one a a0 :
+  N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a (Ndouble_plus_one a0))). intro H0.
-  rewrite (Neqb_complete _ _ H0) in H. rewrite (Ndouble_plus_one_div2 a0) in H.
-  rewrite (Neqb_correct a0) in H. discriminate H.
-  intro H0. rewrite Neqb_comm. assumption.
+  intros H. eqb2eq. contradict H. subst. apply N.div2_succ_double.
 Qed.
 
-Lemma Nbit0_neq :
- forall a a',
-   Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false.
+Lemma Nbit0_neq a a' :
+  N.odd a = false -> N.odd a' = true -> N.eqb a a' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H1.
-  rewrite (Neqb_complete _ _ H1) in H.
-  rewrite H in H0. discriminate H0.
-  trivial.
+  intros. eqb2eq. now intros <-.
 Qed.
 
-Lemma Ndiv2_eq :
- forall a a', Neqb a a' = true -> Neqb (Ndiv2 a) (Ndiv2 a') = true.
+Lemma Ndiv2_eq a a' :
+  N.eqb a a' = true -> N.eqb (N.div2 a) (N.div2 a') = true.
 Proof.
-  intros. cut (a = a'). intros. rewrite H0. apply Neqb_correct.
-  apply Neqb_complete. exact H.
+  intros. eqb2eq. now subst.
 Qed.
 
-Lemma Ndiv2_neq :
- forall a a',
-   Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false.
+Lemma Ndiv2_neq a a' :
+  N.eqb (N.div2 a) (N.div2 a') = false -> N.eqb a a' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete _ _ H0) in H.
-  rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H.
-  trivial.
+  intros H. eqb2eq. contradict H. now subst.
 Qed.
 
-Lemma Ndiv2_bit_eq :
- forall a a',
-   Nbit0 a = Nbit0 a' -> Ndiv2 a = Ndiv2 a' -> a = a'.
+Lemma Ndiv2_bit_eq a a' :
+  N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'.
 Proof.
-  intros. apply Nbit_faithful. unfold eqf in |- *. destruct n.
-  rewrite Nbit0_correct. rewrite Nbit0_correct. assumption.
-  rewrite <- Ndiv2_correct. rewrite <- Ndiv2_correct.
-  rewrite H0. reflexivity.
+  intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'.
 Qed.
 
-Lemma Ndiv2_bit_neq :
- forall a a',
-   Neqb a a' = false ->
-   Nbit0 a = Nbit0 a' -> Neqb (Ndiv2 a) (Ndiv2 a') = false.
+Lemma Ndiv2_bit_neq a a' :
+  N.eqb a a' = false ->
+   N.odd a = N.odd a' -> N.eqb (N.div2 a) (N.div2 a') = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndiv2 a) (Ndiv2 a'))). intro H1.
-  rewrite (Ndiv2_bit_eq _ _ H0 (Neqb_complete _ _ H1)) in H.
-  rewrite (Neqb_correct a') in H. discriminate H.
-  trivial.
+  intros H H'. eqb2eq. contradict H. now apply Ndiv2_bit_eq.
 Qed.
 
-Lemma Nneq_elim :
- forall a a',
-   Neqb a a' = false ->
-   Nbit0 a = negb (Nbit0 a') \/
-   Neqb (Ndiv2 a) (Ndiv2 a') = false.
+Lemma Nneq_elim a a' :
+   N.eqb a a' = false ->
+   N.odd a = negb (N.odd a') \/
+   N.eqb (N.div2 a) (N.div2 a') = false.
 Proof.
-  intros. cut (Nbit0 a = Nbit0 a' \/ Nbit0 a = negb (Nbit0 a')).
+  intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')).
   intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption.
   assumption.
   intro. left. assumption.
-  case (Nbit0 a); case (Nbit0 a'); auto.
+  case (N.odd a), (N.odd a'); auto.
 Qed.
 
-Lemma Ndouble_or_double_plus_un :
- forall a,
-   {a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}.
+Lemma Ndouble_or_double_plus_un a :
+   {a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}.
 Proof.
-  intro. elim (sumbool_of_bool (Nbit0 a)). intro H. right. split with (Ndiv2 a).
-  rewrite (Ndiv2_double_plus_one a H). reflexivity.
-  intro H. left. split with (Ndiv2 a). rewrite (Ndiv2_double a H). reflexivity.
+  elim (sumbool_of_bool (N.odd a)); intros H; [right|left];
+    exists (N.div2 a); symmetry;
+    apply Ndiv2_double_plus_one || apply Ndiv2_double; auto.
 Qed.
 
-(** A boolean order on [N] *)
+(** An inefficient boolean order on [N]. Please use [N.leb] instead now. *)
 
-Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b).
+Definition Nleb (a b:N) := leb (N.to_nat a) (N.to_nat b).
 
-Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b.
+Lemma Nleb_alt a b : Nleb a b = N.leb a b.
 Proof.
- intros; unfold Nle; rewrite nat_of_Ncompare.
- unfold Nleb; apply leb_compare.
+ unfold Nleb.
+ now rewrite eq_iff_eq_true, N.leb_le, leb_compare, <- N2Nat.inj_compare.
 Qed.
 
-Lemma Nleb_refl : forall a, Nleb a a = true.
-Proof.
-  intro. unfold Nleb in |- *. apply leb_correct. apply le_n.
-Qed.
+Lemma Nleb_Nle a b : Nleb a b = true <-> a <= b.
+Proof. now rewrite Nleb_alt, N.leb_le. Qed.
 
-Lemma Nleb_antisym :
- forall a b, Nleb a b = true -> Nleb b a = true -> a = b.
-Proof.
-  unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b).
-  rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity.
-Qed.
+Lemma Nleb_refl a : Nleb a a = true.
+Proof. rewrite Nleb_Nle; apply N.le_refl. Qed.
 
-Lemma Nleb_trans :
- forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
-Proof.
-  unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b).
-  apply leb_complete. assumption.
-  apply leb_complete. assumption.
-Qed.
+Lemma Nleb_antisym a b : Nleb a b = true -> Nleb b a = true -> a = b.
+Proof. rewrite !Nleb_Nle. apply N.le_antisymm. Qed.
+
+Lemma Nleb_trans a b c : Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
+Proof. rewrite !Nleb_Nle. apply N.le_trans. Qed.
 
-Lemma Nleb_ltb_trans :
- forall a b c,
-   Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
+Lemma Nleb_ltb_trans a b c :
+  Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply le_lt_trans with (m := N.to_nat b).
   apply leb_complete. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nltb_leb_trans :
- forall a b c,
-   Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
+Lemma Nltb_leb_trans a b c :
+  Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply lt_le_trans with (m := N.to_nat b).
   apply leb_complete_conv. assumption.
   apply leb_complete. assumption.
 Qed.
 
-Lemma Nltb_trans :
- forall a b c,
-   Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
+Lemma Nltb_trans a b c :
+  Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply lt_trans with (m := N.to_nat b).
   apply leb_complete_conv. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true.
+Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak.
+  unfold Nleb. intros. apply leb_correct. apply lt_le_weak.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nleb_double_mono :
- forall a b,
-   Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true.
+Lemma Nleb_double_mono a b :
+  Nleb a b = true -> Nleb (N.double a) (N.double b) = true.
 Proof.
-  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct.
-  simpl in |- *. apply plus_le_compat. apply leb_complete. assumption.
-  apply plus_le_compat. apply leb_complete. assumption.
-  apply le_n.
+  unfold Nleb. intros. rewrite !N2Nat.inj_double. apply leb_correct.
+  apply mult_le_compat_l. now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_plus_one_mono :
- forall a b,
-   Nleb a b = true ->
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true.
+Lemma Nleb_double_plus_one_mono a b :
+  Nleb a b = true ->
+   Nleb (N.succ_double a) (N.succ_double b) = true.
 Proof.
-  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
-  apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete.
-  assumption.
-  apply plus_le_compat. apply leb_complete. assumption.
-  apply le_n.
+  unfold Nleb. intros. rewrite !N2Nat.inj_succ_double. apply leb_correct.
+  apply le_n_S, mult_le_compat_l. now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_mono_conv :
- forall a b,
-   Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true.
+Lemma Nleb_double_mono_conv a b :
+  Nleb (N.double a) (N.double b) = true -> Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro.
-  apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption.
+  unfold Nleb. rewrite !N2Nat.inj_double. intro. apply leb_correct.
+  apply (mult_S_le_reg_l 1). now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_plus_one_mono_conv :
- forall a b,
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true ->
+Lemma Nleb_double_plus_one_mono_conv a b :
+  Nleb (N.succ_double a) (N.succ_double b) = true ->
    Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
-  intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete.
-  assumption.
+  unfold Nleb. rewrite !N2Nat.inj_succ_double. intro. apply leb_correct.
+  apply (mult_S_le_reg_l 1). apply le_S_n. now apply leb_complete.
 Qed.
 
-Lemma Nltb_double_mono :
- forall a b,
-   Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false.
+Lemma Nltb_double_mono a b :
+   Nleb a b = false -> Nleb (N.double a) (N.double b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0.
+  intros. elim (sumbool_of_bool (Nleb (N.double a) (N.double b))). intro H0.
   rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_plus_one_mono :
- forall a b,
-   Nleb a b = false ->
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false.
+Lemma Nltb_double_plus_one_mono a b :
+  Nleb a b = false ->
+   Nleb (N.succ_double a) (N.succ_double b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0.
+  intros. elim (sumbool_of_bool (Nleb (N.succ_double a) (N.succ_double b))).
+  intro H0.
   rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_mono_conv :
- forall a b,
-   Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false.
+Lemma Nltb_double_mono_conv a b :
+  Nleb (N.double a) (N.double b) = false -> Nleb a b = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H.
-  discriminate H.
+  intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
+  rewrite (Nleb_double_mono _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_plus_one_mono_conv :
- forall a b,
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false ->
+Lemma Nltb_double_plus_one_mono_conv a b :
+  Nleb (N.succ_double a) (N.succ_double b) = false ->
    Nleb a b = false.
 Proof.
   intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
@@ -331,110 +254,52 @@ Proof.
   trivial.
 Qed.
 
-(* Nleb and Ncompare *)
+(* Nleb and N.compare *)
 
-(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt,
+(* NB: No need to prove that Nleb a b = true <-> N.compare a b <> Gt,
    this statement is in fact Nleb_Nle! *)
 
-Lemma Nltb_Ncompare : forall a b,
- Nleb a b = false <-> Ncompare a b = Gt.
+Lemma Nltb_Ncompare a b : Nleb a b = false <-> N.compare a b = Gt.
 Proof.
- intros.
- assert (IFF : forall x:bool, x = false <-> ~ x = true)
-   by (destruct x; intuition).
- rewrite IFF, Nleb_Nle; unfold Nle.
- destruct (Ncompare a b); split; intro H; auto;
-  elim H; discriminate.
+  now rewrite N.compare_nle_iff, <- Nleb_Nle, not_true_iff_false.
 Qed.
 
-Lemma Ncompare_Gt_Nltb : forall a b,
- Ncompare a b = Gt -> Nleb a b = false.
-Proof.
- intros; apply <- Nltb_Ncompare; auto.
-Qed.
+Lemma Ncompare_Gt_Nltb a b : N.compare a b = Gt -> Nleb a b = false.
+Proof. apply <- Nltb_Ncompare; auto. Qed.
 
-Lemma Ncompare_Lt_Nltb : forall a b,
- Ncompare a b = Lt -> Nleb b a = false.
+Lemma Ncompare_Lt_Nltb a b : N.compare a b = Lt -> Nleb b a = false.
 Proof.
- intros a b H.
- rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto.
+ intros H. rewrite Nltb_Ncompare, N.compare_antisym, H; auto.
 Qed.
 
-(* An alternate [min] function over [N] *)
+(* Old results about [N.min] *)
 
-Definition Nmin' (a b:N) := if Nleb a b then a else b.
+Notation Nmin_choice := N.min_dec (compat "8.3").
 
-Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b.
-Proof.
- unfold Nmin, Nmin', Nleb; intros.
- rewrite nat_of_Ncompare.
- generalize (leb_compare (nat_of_N a) (nat_of_N b));
- destruct (nat_compare (nat_of_N a) (nat_of_N b));
- destruct (leb (nat_of_N a) (nat_of_N b)); intuition.
- lapply H1; intros; discriminate.
- lapply H1; intros; discriminate.
-Qed.
+Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true.
+Proof. rewrite Nleb_Nle. apply N.le_min_l. Qed.
 
-Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}.
-Proof.
-  unfold Nmin in *; intros; destruct (Ncompare a b); auto.
-Qed.
+Lemma Nmin_le_2 a b : Nleb (N.min a b) b = true.
+Proof. rewrite Nleb_Nle. apply N.le_min_r. Qed.
 
-Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true.
-Proof.
-  intros; rewrite Nmin_Nmin'.
-  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H.
-  apply Nleb_refl.
-  intro H. rewrite H. apply Nltb_leb_weak. assumption.
-Qed.
+Lemma Nmin_le_3 a b c : Nleb a (N.min b c) = true -> Nleb a b = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb_l. Qed.
 
-Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true.
-Proof.
-  intros; rewrite Nmin_Nmin'.
-  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption.
-  intro H. rewrite H. apply Nleb_refl.
-Qed.
+Lemma Nmin_le_4 a b c : Nleb a (N.min b c) = true -> Nleb a c = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb_r. Qed.
 
-Lemma Nmin_le_3 :
- forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true.
-Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  assumption.
-  intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption.
-Qed.
+Lemma Nmin_le_5 a b c :
+   Nleb a b = true -> Nleb a c = true -> Nleb a (N.min b c) = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb. Qed.
 
-Lemma Nmin_le_4 :
- forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true.
+Lemma Nmin_lt_3 a b c : Nleb (N.min b c) a = false -> Nleb b a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  apply Nleb_trans with (b := b); assumption.
-  intro H0. rewrite H0 in H. assumption.
-Qed.
-
-Lemma Nmin_le_5 :
- forall a b c,
-   Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true.
-Proof.
-  intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption.
-  intro H1. rewrite H1. assumption.
-Qed.
-
-Lemma Nmin_lt_3 :
- forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false.
-Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  assumption.
-  intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption.
+  rewrite <- !not_true_iff_false, !Nleb_Nle.
+  rewrite N.min_le_iff; auto.
 Qed.
 
-Lemma Nmin_lt_4 :
- forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false.
+Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  apply Nltb_leb_trans with (b := b); assumption.
-  intro H0. rewrite H0 in H. assumption.
+  rewrite <- !not_true_iff_false, !Nleb_Nle.
+  rewrite N.min_le_iff; auto.
 Qed.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index b0c33595..4ea8e1d4 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.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        *)
@@ -15,41 +15,41 @@ Local Open Scope N_scope.
 
 (** Compatibility names for some bitwise operations *)
 
-Notation Pxor := Pos.lxor (only parsing).
-Notation Nxor := N.lxor (only parsing).
-Notation Pbit := Pos.testbit_nat (only parsing).
-Notation Nbit := N.testbit_nat (only parsing).
+Notation Pxor := Pos.lxor (compat "8.3").
+Notation Nxor := N.lxor (compat "8.3").
+Notation Pbit := Pos.testbit_nat (compat "8.3").
+Notation Nbit := N.testbit_nat (compat "8.3").
 
-Notation Nxor_eq := N.lxor_eq (only parsing).
-Notation Nxor_comm := N.lxor_comm (only parsing).
-Notation Nxor_assoc := N.lxor_assoc (only parsing).
-Notation Nxor_neutral_left := N.lxor_0_l (only parsing).
-Notation Nxor_neutral_right := N.lxor_0_r (only parsing).
-Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing).
+Notation Nxor_eq := N.lxor_eq (compat "8.3").
+Notation Nxor_comm := N.lxor_comm (compat "8.3").
+Notation Nxor_assoc := N.lxor_assoc (compat "8.3").
+Notation Nxor_neutral_left := N.lxor_0_l (compat "8.3").
+Notation Nxor_neutral_right := N.lxor_0_r (compat "8.3").
+Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3").
 
 (** Equivalence of bit-testing functions,
     either with index in [N] or in [nat]. *)
 
 Lemma Ptestbit_Pbit :
- forall p n, Pos.testbit p (N.of_nat n) = Pbit p n.
+ forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n.
 Proof.
  induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial;
-  rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred.
+  rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred.
 Qed.
 
-Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n.
+Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n.
 Proof.
  destruct a. trivial. apply Ptestbit_Pbit.
 Qed.
 
 Lemma Pbit_Ptestbit :
- forall p n, Pbit p (N.to_nat n) = Pos.testbit p n.
+ forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n.
 Proof.
  intros; now rewrite <- Ptestbit_Pbit, N2Nat.id.
 Qed.
 
 Lemma Nbit_Ntestbit :
- forall a n, Nbit a (N.to_nat n) = N.testbit a n.
+ forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n.
 Proof.
  destruct a. trivial. apply Pbit_Ptestbit.
 Qed.
@@ -73,7 +73,7 @@ Lemma Nshiftr_nat_equiv :
 Proof.
  intros a [|n]; simpl. unfold N.shiftr_nat.
  trivial.
- symmetry. apply iter_nat_of_P.
+ symmetry. apply Pos2Nat.inj_iter.
 Qed.
 
 Lemma Nshiftr_equiv_nat :
@@ -99,7 +99,7 @@ Qed.
 (** Correctness proofs for shifts, nat version *)
 
 Lemma Nshiftr_nat_spec : forall a n m,
-  Nbit (N.shiftr_nat a n) m = Nbit a (m+n).
+  N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n).
 Proof.
  induction n; intros m.
  now rewrite <- plus_n_O.
@@ -108,7 +108,7 @@ Proof.
 Qed.
 
 Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
-  Nbit (N.shiftl_nat a n) m = Nbit a (m-n).
+  N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).
 Proof.
  induction n; intros m H.
  now rewrite <- minus_n_O.
@@ -118,7 +118,7 @@ Proof.
 Qed.
 
 Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
- Nbit (N.shiftl_nat a n) m = false.
+ N.testbit_nat (N.shiftl_nat a n) m = false.
 Proof.
  induction n; intros m H. inversion H.
  rewrite Nshiftl_nat_S.
@@ -151,52 +151,52 @@ Proof.
  rewrite 2 Pshiftl_nat_S. now f_equal.
 Qed.
 
-(** Semantics of bitwise operations with respect to [Nbit] *)
+(** Semantics of bitwise operations with respect to [N.testbit_nat] *)
 
 Lemma Pxor_semantics p p' n :
- Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n).
+ N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec.
 Qed.
 
 Lemma Nxor_semantics a a' n :
- Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n).
+ N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.lxor_spec.
 Qed.
 
 Lemma Por_semantics p p' n :
- Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n).
+ Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n).
 Proof.
  rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec.
 Qed.
 
 Lemma Nor_semantics a a' n :
- Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n).
+ N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.lor_spec.
 Qed.
 
 Lemma Pand_semantics p p' n :
- Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n).
+ N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec.
 Qed.
 
 Lemma Nand_semantics a a' n :
- Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n).
+ N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.land_spec.
 Qed.
 
 Lemma Pdiff_semantics p p' n :
- Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n).
+ N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec.
 Qed.
 
 Lemma Ndiff_semantics a a' n :
- Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n).
+ N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec.
 Qed.
@@ -213,13 +213,13 @@ Local Infix "==" := eqf (at level 70, no associativity).
 
 Local Notation Step H := (fun n => H (S n)).
 
-Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)).
+Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)).
 Proof.
  induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
   apply (IHp (Step H)).
 Qed.
 
-Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
+Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'.
 Proof.
  induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial;
   try discriminate (H O).
@@ -229,7 +229,7 @@ Proof.
  symmetry in H. destruct (Pbit_faithful_0 _ (Step H)).
 Qed.
 
-Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
+Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'.
 Proof.
  intros [|p] [|p'] H; trivial.
  symmetry in H. destruct (Pbit_faithful_0 _ H).
@@ -237,7 +237,7 @@ Proof.
  f_equal. apply Pbit_faithful, H.
 Qed.
 
-Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
+Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'.
 Proof.
  split. apply Nbit_faithful. intros; now subst.
 Qed.
@@ -247,30 +247,30 @@ Local Close Scope N_scope.
 (** Checking whether a number is odd, i.e.
    if its lower bit is set. *)
 
-Notation Nbit0 := N.odd (only parsing).
+Notation Nbit0 := N.odd (compat "8.3").
 
-Definition Nodd (n:N) := Nbit0 n = true.
-Definition Neven (n:N) := Nbit0 n = false.
+Definition Nodd (n:N) := N.odd n = true.
+Definition Neven (n:N) := N.odd n = false.
 
-Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n.
+Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n.
 Proof.
   destruct n; trivial.
   destruct p; trivial.
 Qed.
 
-Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false.
+Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false.
 Proof.
   destruct n; trivial.
 Qed.
 
 Lemma Ndouble_plus_one_bit0 :
- forall n:N, Nbit0 (Ndouble_plus_one n) = true.
+ forall n:N, N.odd (N.succ_double n) = true.
 Proof.
   destruct n; trivial.
 Qed.
 
 Lemma Ndiv2_double :
- forall n:N, Neven n -> Ndouble (Ndiv2 n) = n.
+ forall n:N, Neven n -> N.double (N.div2 n) = n.
 Proof.
   destruct n. trivial. destruct p. intro H. discriminate H.
   intros. reflexivity.
@@ -278,7 +278,7 @@ Proof.
 Qed.
 
 Lemma Ndiv2_double_plus_one :
- forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n.
+ forall n:N, Nodd n -> N.succ_double (N.div2 n) = n.
 Proof.
   destruct n. intro. discriminate H.
   destruct p. intros. reflexivity.
@@ -287,31 +287,31 @@ Proof.
 Qed.
 
 Lemma Ndiv2_correct :
- forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit a (S n).
+ forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n).
 Proof.
   destruct a; trivial.
   destruct p; trivial.
 Qed.
 
 Lemma Nxor_bit0 :
- forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a').
+ forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a').
 Proof.
   intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O).
   rewrite Nbit0_correct, Nbit0_correct. reflexivity.
 Qed.
 
 Lemma Nxor_div2 :
- forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a').
+ forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a').
 Proof.
   intros. apply Nbit_faithful. unfold eqf. intro.
-  rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
+  rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
   rewrite 2! Ndiv2_correct.
   reflexivity.
 Qed.
 
 Lemma Nneg_bit0 :
  forall a a':N,
-   Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
+   N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a').
 Proof.
   intros.
   rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, 
@@ -320,24 +320,24 @@ Proof.
 Qed.
 
 Lemma Nneg_bit0_1 :
- forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 a').
+ forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a').
 Proof.
   intros. apply Nneg_bit0. rewrite H. reflexivity.
 Qed.
 
 Lemma Nneg_bit0_2 :
  forall (a a':N) (p:positive),
-   Nxor a a' = Npos (xI p) -> Nbit0 a = negb (Nbit0 a').
+   N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a').
 Proof.
   intros. apply Nneg_bit0. rewrite H. reflexivity.
 Qed.
 
 Lemma Nsame_bit0 :
  forall (a a':N) (p:positive),
-   Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'.
+   N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'.
 Proof.
-  intros. rewrite <- (xorb_false (Nbit0 a)).
-  assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
+  intros. rewrite <- (xorb_false (N.odd a)).
+  assert (H0: N.odd (Npos (xO p)) = false) by reflexivity.
   rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb.
     reflexivity.
 Qed.
@@ -346,77 +346,77 @@ Qed.
 
 Fixpoint Nless_aux (a a':N) (p:positive) : bool :=
   match p with
-  | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p'
-  | _ => andb (negb (Nbit0 a)) (Nbit0 a')
+  | xO p' => Nless_aux (N.div2 a) (N.div2 a') p'
+  | _ => andb (negb (N.odd a)) (N.odd a')
   end.
 
 Definition Nless (a a':N) :=
-  match Nxor a a' with
+  match N.lxor a a' with
   | N0 => false
   | Npos p => Nless_aux a a' p
   end.
 
 Lemma Nbit0_less :
  forall a a',
-   Nbit0 a = false -> Nbit0 a' = true -> Nless a a' = true.
+   N.odd a = false -> N.odd a' = true -> Nless a a' = true.
 Proof.
-  intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+  intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
   rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
-  assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
 Lemma Nbit0_gt :
  forall a a',
-   Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false.
+   N.odd a = true -> N.odd a' = false -> Nless a a' = false.
 Proof.
-  intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+  intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
   rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
-  assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
 Lemma Nless_not_refl : forall a, Nless a a = false.
 Proof.
-  intro. unfold Nless. rewrite (Nxor_nilpotent a). reflexivity.
+  intro. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity.
 Qed.
 
 Lemma Nless_def_1 :
- forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'.
+ forall a a', Nless (N.double a) (N.double a') = Nless a a'.
 Proof.
   destruct a; destruct a'. reflexivity.
   trivial.
   unfold Nless. simpl. destruct p; trivial.
-  unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+  unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
   trivial.
 Qed.
 
 Lemma Nless_def_2 :
  forall a a',
-   Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'.
+   Nless (N.succ_double a) (N.succ_double a') = Nless a a'.
 Proof.
   destruct a; destruct a'. reflexivity.
   trivial.
   unfold Nless. simpl. destruct p; trivial.
-  unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+  unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
   trivial.
 Qed.
 
 Lemma Nless_def_3 :
- forall a a', Nless (Ndouble a) (Ndouble_plus_one a') = true.
+ forall a a', Nless (N.double a) (N.succ_double a') = true.
 Proof.
   intros. apply Nbit0_less. apply Ndouble_bit0.
   apply Ndouble_plus_one_bit0.
 Qed.
 
 Lemma Nless_def_4 :
- forall a a', Nless (Ndouble_plus_one a) (Ndouble a') = false.
+ forall a a', Nless (N.succ_double a) (N.double a') = false.
 Proof.
   intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0.
   apply Ndouble_bit0.
@@ -425,7 +425,7 @@ Qed.
 Lemma Nless_z : forall a, Nless a N0 = false.
 Proof.
   induction a. reflexivity.
-  unfold Nless. rewrite (Nxor_neutral_right (Npos p)). induction p; trivial.
+  unfold Nless. rewrite (N.lxor_0_r (Npos p)). induction p; trivial.
 Qed.
 
 Lemma N0_less_1 :
@@ -445,26 +445,26 @@ Lemma Nless_trans :
  forall a a' a'',
    Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
 Proof.
-  induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
+  induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0.
     case_eq (Nless N0 a'') ; intros Heqn. trivial.
      rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
-    induction a' as [|a' _|a' _] using N_ind_double.
-      rewrite (Nless_z (Ndouble a)) in H. discriminate H.
+    induction a' as [|a' _|a' _] using N.binary_ind.
+      rewrite (Nless_z (N.double a)) in H. discriminate H.
       rewrite (Nless_def_1 a a') in H.
-       induction a'' using N_ind_double.
-         rewrite (Nless_z (Ndouble a')) in H0. discriminate H0.
+       induction a'' using N.binary_ind.
+         rewrite (Nless_z (N.double a')) in H0. discriminate H0.
          rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
           exact (IHa _ _ H H0).
          apply Nless_def_3.
-      induction a'' as [|a'' _|a'' _] using N_ind_double.
-        rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+      induction a'' as [|a'' _|a'' _] using N.binary_ind.
+        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
         rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
         apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N_ind_double.
-      rewrite (Nless_z (Ndouble_plus_one a)) in H. discriminate H.
+    induction a' as [|a' _|a' _] using N.binary_ind.
+      rewrite (Nless_z (N.succ_double a)) in H. discriminate H.
       rewrite (Nless_def_4 a a') in H. discriminate H.
-      induction a'' using N_ind_double.
-        rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+      induction a'' using N.binary_ind.
+        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
         rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
         rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
           rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
@@ -473,17 +473,17 @@ Qed.
 Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
-  induction a using N_rec_double; intro a'.
+  induction a using N.binary_rec; intro a'.
     case_eq (Nless N0 a') ; intros Heqb. left. left. auto.
      right. rewrite (N0_less_2 a' Heqb). reflexivity.
-    induction a' as [|a' _|a' _] using N_rec_double.
-      case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto.
+    induction a' as [|a' _|a' _] using N.binary_rec.
+      case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto.
        right. exact (N0_less_2 _  Heqb).
       rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
         left. assumption.
         right. reflexivity.
     left. left. apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N_rec_double.
+    induction a' as [|a' _|a' _] using N.binary_rec.
       left. right. destruct a; reflexivity.
       left. right. apply Nless_def_3.
       rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
@@ -493,19 +493,19 @@ Qed.
 
 (** Number of digits in a number *)
 
-Notation Nsize := N.size_nat (only parsing).
+Notation Nsize := N.size_nat (compat "8.3").
 
 (** conversions between N and bit vectors. *)
 
-Fixpoint P2Bv (p:positive) : Bvector (Psize p) :=
- match p return Bvector (Psize p) with
+Fixpoint P2Bv (p:positive) : Bvector (Pos.size_nat p) :=
+ match p return Bvector (Pos.size_nat p) with
    | xH => Bvect_true 1%nat
-   | xO p => Bcons false (Psize p) (P2Bv p)
-   | xI p => Bcons true (Psize p) (P2Bv p)
+   | xO p => Bcons false (Pos.size_nat p) (P2Bv p)
+   | xI p => Bcons true (Pos.size_nat p) (P2Bv p)
  end.
 
-Definition N2Bv (n:N) : Bvector (Nsize n) :=
-  match n as n0 return Bvector (Nsize n0) with
+Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
+  match n as n0 return Bvector (N.size_nat n0) with
     | N0 => Bnil
     | Npos p => P2Bv p
   end.
@@ -513,8 +513,8 @@ Definition N2Bv (n:N) : Bvector (Nsize n) :=
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vector.nil => N0
-    | Vector.cons false n bv => Ndouble (Bv2N n bv)
-    | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv)
+    | Vector.cons false n bv => N.double (Bv2N n bv)
+    | Vector.cons true n bv => N.succ_double (Bv2N n bv)
   end.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
@@ -528,7 +528,7 @@ Qed.
   bit vector has some zeros on its right, they will disappear during
   the return [Bv2N] translation: *)
 
-Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.
+Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n.
 Proof.
 induction bv; intros.
 auto.
@@ -543,7 +543,7 @@ Qed.
 
 Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
   Bsign _ bv = true <->
-  Nsize (Bv2N _ bv) = (S n).
+  N.size_nat (Bv2N _ bv) = (S n).
 Proof.
 apply Vector.rectS ; intros ; simpl.
 destruct a ; compute ; split ; intros x ; now inversion x.
@@ -567,7 +567,7 @@ Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
 
 (** The first [N2Bv] is then a special case of [N2Bv_gen] *)
 
-Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (Nsize a) a.
+Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a.
 Proof.
 destruct a; simpl.
 auto.
@@ -578,7 +578,7 @@ Qed.
    [a] plus some zeros. *)
 
 Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
- N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k).
+ N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k).
 Proof.
 destruct a; simpl.
 destruct k; simpl; auto.
@@ -603,7 +603,7 @@ Qed.
 (** accessing some precise bits. *)
 
 Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
-  Nbit0 (Bv2N _ bv) = Blow _ bv.
+  N.odd (Bv2N _ bv) = Blow _ bv.
 Proof.
 apply Vector.caseS.
 intros.
@@ -616,7 +616,7 @@ Qed.
 Notation Bnth := (@Vector.nth_order bool).
 
 Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
-  Bnth bv H = Nbit (Bv2N _ bv) p.
+  Bnth bv H = N.testbit_nat (Bv2N _ bv) p.
 Proof.
 induction bv; intros.
 inversion H.
@@ -626,7 +626,7 @@ destruct p ; simpl.
     simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
 Qed.
 
-Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false.
+Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false.
 Proof.
 destruct n as [|n].
 simpl; auto.
@@ -635,7 +635,8 @@ inversion H.
 inversion H.
 Qed.
 
-Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H.
+Lemma Nbit_Bth: forall n p (H:p < N.size_nat n),
+  N.testbit_nat n p = Bnth (N2Bv n) H.
 Proof.
 destruct n as [|n].
 inversion H.
@@ -646,7 +647,7 @@ Qed.
 (** Binary bitwise operations are the same in the two worlds. *)
 
 Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
-  Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
+  Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv').
 Proof.
 apply Vector.rect2 ; intros.
 now simpl.
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 22adc505..ce4f7663 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.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        *)
@@ -33,12 +33,12 @@ Definition Nplength (a:N) :=
 Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.
 Proof.
   simple induction a; trivial.
-  unfold Nplength in |- *; intros; discriminate H.
+  unfold Nplength; intros; discriminate H.
 Qed.
 
 Lemma Nplength_zeros :
  forall (a:N) (n:nat),
-   Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false.
+   Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false.
 Proof.
   simple induction a; trivial.
   simple induction p. simple induction n. intros. inversion H1.
@@ -46,33 +46,33 @@ Proof.
   intros. simpl in H1. discriminate H1.
   simple induction k. trivial.
   generalize H0. case n. intros. inversion H3.
-  intros. simpl in |- *. unfold Nbit in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
+  intros. simpl. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
   exact (lt_S_n n1 n0 H3).
-  simpl in |- *. intros n H. inversion H. intros. inversion H0.
+  simpl. intros n H. inversion H. intros. inversion H0.
 Qed.
 
 Lemma Nplength_one :
- forall (a:N) (n:nat), Nplength a = ni n -> Nbit a n = true.
+ forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true.
 Proof.
   simple induction a. intros. inversion H.
   simple induction p. intros. simpl in H0. inversion H0. reflexivity.
-  intros. simpl in H0. inversion H0. simpl in |- *. unfold Nbit in H. apply H. reflexivity.
+  intros. simpl in H0. inversion H0. simpl. unfold N.testbit_nat in H. apply H. reflexivity.
   intros. simpl in H. inversion H. reflexivity.
 Qed.
 
 Lemma Nplength_first_one :
  forall (a:N) (n:nat),
-   (forall k:nat, k < n -> Nbit a k = false) ->
-   Nbit a n = true -> Nplength a = ni n.
+   (forall k:nat, k < n -> N.testbit_nat a k = false) ->
+   N.testbit_nat a n = true -> Nplength a = ni n.
 Proof.
   simple induction a. intros. simpl in H0. discriminate H0.
   simple induction p. intros. generalize H0. case n. intros. reflexivity.
-  intros. absurd (Nbit (Npos (xI p0)) 0 = false). trivial with bool.
+  intros. absurd (N.testbit_nat (Npos (xI p0)) 0 = false). trivial with bool.
   auto with bool arith.
   intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3.
-  intros. simpl in |- *. unfold Nplength in H.
+  intros. simpl. unfold Nplength in H.
   cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity.
-  apply H. intros. change (Nbit (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4.
+  apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4.
   exact H3.
   intro. case n. trivial.
   intros. simpl in H0. discriminate H0.
@@ -90,10 +90,10 @@ Definition ni_min (d d':natinf) :=
 Lemma ni_min_idemp : forall d:natinf, ni_min d d = d.
 Proof.
   simple induction d; trivial.
-  unfold ni_min in |- *.
+  unfold ni_min.
   simple induction n; trivial.
   intros.
-  simpl in |- *.
+  simpl.
   inversion H.
   rewrite H1.
   rewrite H1.
@@ -105,7 +105,7 @@ Proof.
   simple induction d. simple induction d'; trivial.
   simple induction d'; trivial. elim n. simple induction n0; trivial.
   intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0).
-  intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity.
+  intro. unfold ni_min. simpl. rewrite H1. reflexivity.
   cut (ni (min n0 n2) = ni (min n2 n0)). intros.
   inversion H1; trivial.
   exact (H n2).
@@ -116,11 +116,11 @@ Lemma ni_min_assoc :
 Proof.
   simple induction d; trivial. simple induction d'; trivial.
   simple induction d''; trivial.
-  unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)).
+  unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)).
   intro. rewrite H. reflexivity.
   generalize n0 n1. elim n; trivial.
   simple induction n3; trivial. simple induction n5; trivial.
-  intros. simpl in |- *. auto.
+  intros. simpl. auto.
 Qed.
 
 Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0.
@@ -152,42 +152,42 @@ Qed.
 
 Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'.
 Proof.
-  unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial.
+  unfold ni_le. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial.
 Qed.
 
 Lemma ni_le_trans :
  forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''.
 Proof.
-  unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity.
+  unfold ni_le. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity.
 Qed.
 
 Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d.
 Proof.
-  unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc.
+  unfold ni_le. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc.
   rewrite ni_min_idemp. reflexivity.
 Qed.
 
 Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'.
 Proof.
-  unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity.
+  unfold ni_le. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity.
 Qed.
 
 Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'.
 Proof.
   simple induction d. intro. right. exact (ni_min_inf_l d').
   simple induction d'. left. exact (ni_min_inf_r (ni n)).
-  unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0).
+  unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0).
   intros. case (H n0). intro. left. rewrite H0. reflexivity.
   intro. right. rewrite H0. reflexivity.
   elim n. intro. left. reflexivity.
   simple induction n1. right. reflexivity.
-  intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity.
-  intro. right. simpl in |- *. rewrite H1. reflexivity.
+  intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity.
+  intro. right. simpl. rewrite H1. reflexivity.
 Qed.
 
 Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d.
 Proof.
-  unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case.
+  unfold ni_le. intros. rewrite (ni_min_comm d' d). apply ni_min_case.
 Qed.
 
 Lemma ni_le_min_induc :
@@ -201,7 +201,7 @@ Proof.
   apply ni_le_antisym. apply H1. apply ni_le_refl.
   exact H2.
   exact H.
-  intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2.
+  intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le. rewrite ni_min_comm. exact H2.
   apply ni_le_refl.
   exact H0.
 Qed.
@@ -209,40 +209,40 @@ Qed.
 Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n).
 Proof.
   cut (forall m n:nat, m <= n -> min m n = m).
-  intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity.
+  intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity.
   simple induction m. trivial.
   simple induction n0. intro. inversion H0.
-  intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity.
+  intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity.
 Qed.
 
 Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n.
 Proof.
-  unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r.
+  unfold ni_le. unfold ni_min. intros. inversion H. apply le_min_r.
 Qed.
 
 Lemma Nplength_lb :
  forall (a:N) (n:nat),
-   (forall k:nat, k < n -> Nbit a k = false) -> ni_le (ni n) (Nplength a).
+   (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a).
 Proof.
   simple induction a. intros. exact (ni_min_inf_r (ni n)).
-  intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial.
-  intro. absurd (Nbit (Npos p) (Pplength p) = false).
+  intros. unfold Nplength. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial.
+  intro. absurd (N.testbit_nat (Npos p) (Pplength p) = false).
   rewrite
    (Nplength_one (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p)))).
+      (eq_refl (Nplength (Npos p)))).
   discriminate.
   apply H. exact H0.
 Qed.
 
 Lemma Nplength_ub :
- forall (a:N) (n:nat), Nbit a n = true -> ni_le (Nplength a) (ni n).
+ forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n).
 Proof.
   simple induction a. intros. discriminate H.
-  intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial.
-  intro. absurd (Nbit (Npos p) n = true).
+  intros. unfold Nplength. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial.
+  intro. absurd (N.testbit_nat (Npos p) n = true).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p))) n H0).
+      (eq_refl (Nplength (Npos p))) n H0).
   discriminate.
   exact H.
 Qed.
@@ -255,26 +255,26 @@ Qed.
     Instead of working with $d$, we work with $pd$, namely
     [Npdist]: *)
 
-Definition Npdist (a a':N) := Nplength (Nxor a a').
+Definition Npdist (a a':N) := Nplength (N.lxor a a').
 
 (** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that
     $pd(a,a')=infty$ iff $a=a'$: *)
 
 Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.
 Proof.
-  intros. unfold Npdist in |- *. rewrite Nxor_nilpotent. reflexivity.
+  intros. unfold Npdist. rewrite N.lxor_nilpotent. reflexivity.
 Qed.
 
 Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.
 Proof.
-  intros. apply Nxor_eq. apply Nplength_infty. exact H.
+  intros. apply N.lxor_eq. apply Nplength_infty. exact H.
 Qed.
 
 (** $d$ is a distance, so $d(a,a')=d(a',a)$: *)
 
 Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a.
 Proof.
-  unfold Npdist in |- *. intros. rewrite Nxor_comm. reflexivity.
+  unfold Npdist. intros. rewrite N.lxor_comm. reflexivity.
 Qed.
 
 (** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq
@@ -292,21 +292,21 @@ Qed.
 Lemma Nplength_ultra_1 :
  forall a a':N,
    ni_le (Nplength a) (Nplength a') ->
-   ni_le (Nplength a) (Nplength (Nxor a a')).
+   ni_le (Nplength a) (Nplength (N.lxor a a')).
 Proof.
   simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H.
   rewrite (ni_min_inf_l (Nplength a')) in H.
-  rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl.
-  intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros.
-  cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false).
+  rewrite (Nplength_infty a' H). simpl. apply ni_le_refl.
+  intros. unfold Nplength at 1. apply Nplength_lb. intros.
+  cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false).
   intros. apply H1. reflexivity.
   intro a''. case a''. intro. reflexivity.
   intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p))) k H0).
+      (eq_refl (Nplength (Npos p))) k H0).
   generalize H. case a'. trivial.
-  intros. cut (Nbit (Npos p1) k = false). intros. rewrite H3. reflexivity.
+  intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity.
   apply Nplength_zeros with (n := Pplength p1). reflexivity.
   apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0.
   apply ni_le_le. exact H2.
@@ -314,14 +314,14 @@ Qed.
 
 Lemma Nplength_ultra :
  forall a a':N,
-   ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (Nxor a a')).
+   ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')).
 Proof.
   intros. case (ni_le_total (Nplength a) (Nplength a')). intro.
   cut (ni_min (Nplength a) (Nplength a') = Nplength a).
   intro. rewrite H0. apply Nplength_ultra_1. exact H.
   exact H.
   intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a').
-  intro. rewrite H0. rewrite Nxor_comm. apply Nplength_ultra_1. exact H.
+  intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H.
   rewrite ni_min_comm. exact H.
 Qed.
 
@@ -329,8 +329,8 @@ Lemma Npdist_ultra :
  forall a a' a'':N,
    ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').
 Proof.
-  intros. unfold Npdist in |- *. cut (Nxor (Nxor a a'') (Nxor a'' a') = Nxor a a').
+  intros. unfold Npdist. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a').
   intro. rewrite <- H. apply Nplength_ultra.
-  rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent.
-  rewrite Nxor_neutral_left. reflexivity.
+  rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent.
+  rewrite N.lxor_0_l. reflexivity.
 Qed.
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 559f01f1..0b220f5d 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.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        *)
@@ -22,10 +22,10 @@ Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
 Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
 
-Notation Ndiv_eucl := N.div_eucl (only parsing).
-Notation Ndiv := N.div (only parsing).
-Notation Nmod := N.modulo (only parsing).
+Notation Ndiv_eucl := N.div_eucl (compat "8.3").
+Notation Ndiv := N.div (compat "8.3").
+Notation Nmod := N.modulo (compat "8.3").
 
-Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
-Notation Ndiv_mod_eq := N.div_mod' (only parsing).
-Notation Nmod_lt := N.mod_lt (only parsing).
+Notation Ndiv_eucl_correct := N.div_eucl_spec (compat "8.3").
+Notation Ndiv_mod_eq := N.div_mod' (compat "8.3").
+Notation Nmod_lt := N.mod_lt (compat "8.3").
diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v
index 13211f46..737cd450 100644
--- a/theories/NArith/Ngcd_def.v
+++ b/theories/NArith/Ngcd_def.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/NArith/Nnat.v b/theories/NArith/Nnat.v
index 133d4c23..1b7e2f24 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.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        *)
@@ -203,30 +203,30 @@ Hint Rewrite Nat2N.id : Nnat.
 
 (** Compatibility notations *)
 
-Notation nat_of_N_inj := N2Nat.inj (only parsing).
-Notation N_of_nat_of_N := N2Nat.id (only parsing).
-Notation nat_of_Ndouble := N2Nat.inj_double (only parsing).
-Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing).
-Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing).
-Notation nat_of_Nplus := N2Nat.inj_add (only parsing).
-Notation nat_of_Nmult := N2Nat.inj_mul (only parsing).
-Notation nat_of_Nminus := N2Nat.inj_sub (only parsing).
-Notation nat_of_Npred := N2Nat.inj_pred (only parsing).
-Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing).
-Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing).
-Notation nat_of_Nmax := N2Nat.inj_max (only parsing).
-Notation nat_of_Nmin := N2Nat.inj_min (only parsing).
-
-Notation nat_of_N_of_nat := Nat2N.id (only parsing).
-Notation N_of_nat_inj := Nat2N.inj (only parsing).
-Notation N_of_double := Nat2N.inj_double (only parsing).
-Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing).
-Notation N_of_S := Nat2N.inj_succ (only parsing).
-Notation N_of_pred := Nat2N.inj_pred (only parsing).
-Notation N_of_plus := Nat2N.inj_add (only parsing).
-Notation N_of_minus := Nat2N.inj_sub (only parsing).
-Notation N_of_mult := Nat2N.inj_mul (only parsing).
-Notation N_of_div2 := Nat2N.inj_div2 (only parsing).
-Notation N_of_nat_compare := Nat2N.inj_compare (only parsing).
-Notation N_of_min := Nat2N.inj_min (only parsing).
-Notation N_of_max := Nat2N.inj_max (only parsing).
+Notation nat_of_N_inj := N2Nat.inj (compat "8.3").
+Notation N_of_nat_of_N := N2Nat.id (compat "8.3").
+Notation nat_of_Ndouble := N2Nat.inj_double (compat "8.3").
+Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (compat "8.3").
+Notation nat_of_Nsucc := N2Nat.inj_succ (compat "8.3").
+Notation nat_of_Nplus := N2Nat.inj_add (compat "8.3").
+Notation nat_of_Nmult := N2Nat.inj_mul (compat "8.3").
+Notation nat_of_Nminus := N2Nat.inj_sub (compat "8.3").
+Notation nat_of_Npred := N2Nat.inj_pred (compat "8.3").
+Notation nat_of_Ndiv2 := N2Nat.inj_div2 (compat "8.3").
+Notation nat_of_Ncompare := N2Nat.inj_compare (compat "8.3").
+Notation nat_of_Nmax := N2Nat.inj_max (compat "8.3").
+Notation nat_of_Nmin := N2Nat.inj_min (compat "8.3").
+
+Notation nat_of_N_of_nat := Nat2N.id (compat "8.3").
+Notation N_of_nat_inj := Nat2N.inj (compat "8.3").
+Notation N_of_double := Nat2N.inj_double (compat "8.3").
+Notation N_of_double_plus_one := Nat2N.inj_succ_double (compat "8.3").
+Notation N_of_S := Nat2N.inj_succ (compat "8.3").
+Notation N_of_pred := Nat2N.inj_pred (compat "8.3").
+Notation N_of_plus := Nat2N.inj_add (compat "8.3").
+Notation N_of_minus := Nat2N.inj_sub (compat "8.3").
+Notation N_of_mult := Nat2N.inj_mul (compat "8.3").
+Notation N_of_div2 := Nat2N.inj_div2 (compat "8.3").
+Notation N_of_nat_compare := Nat2N.inj_compare (compat "8.3").
+Notation N_of_min := Nat2N.inj_min (compat "8.3").
+Notation N_of_max := Nat2N.inj_max (compat "8.3").
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index edb6b289..240d7469 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.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        *)
@@ -11,8 +11,8 @@ Require Import BinNat.
 (** Obsolete file, see [BinNat] now,
     only compatibility notations remain here. *)
 
-Notation Nsqrtrem := N.sqrtrem (only parsing).
-Notation Nsqrt := N.sqrt (only parsing).
-Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing).
-Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
-Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing).
+Notation Nsqrtrem := N.sqrtrem (compat "8.3").
+Notation Nsqrt := N.sqrt (compat "8.3").
+Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.3").
+Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (compat "8.3").
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.3").