Imported Upstream version 8.4dfsgupstream/8.4dfsg

5 files changed, 226 insertions, 228 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 2e4d52a2..4747cfe1 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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        *)
@@ -1484,8 +1484,7 @@ Qed.
 
 (** We hence obtain all the generic properties of [min] and [max]. *)
 
-Include !UsualMinMaxLogicalProperties.
-Include !UsualMinMaxDecProperties.
+Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 (** Minimum, maximum and constant one *)
 
@@ -1871,183 +1870,184 @@ Notation xI := xI (only parsing).
 Notation xO := xO (only parsing).
 Notation xH := xH (only parsing).
 
-Notation Psucc := Pos.succ (only parsing).
-Notation Pplus := Pos.add (only parsing).
-Notation Pplus_carry := Pos.add_carry (only parsing).
-Notation Ppred := Pos.pred (only parsing).
-Notation Piter_op := Pos.iter_op (only parsing).
-Notation Piter_op_succ := Pos.iter_op_succ (only parsing).
-Notation Pmult_nat := (Pos.iter_op plus) (only parsing).
-Notation nat_of_P := Pos.to_nat (only parsing).
-Notation P_of_succ_nat := Pos.of_succ_nat (only parsing).
-Notation Pdouble_minus_one := Pos.pred_double (only parsing).
-Notation positive_mask := Pos.mask (only parsing).
 Notation IsNul := Pos.IsNul (only parsing).
 Notation IsPos := Pos.IsPos (only parsing).
 Notation IsNeg := Pos.IsNeg (only parsing).
-Notation positive_mask_rect := Pos.mask_rect (only parsing).
-Notation positive_mask_ind := Pos.mask_ind (only parsing).
-Notation positive_mask_rec := Pos.mask_rec (only parsing).
-Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing).
-Notation Pdouble_mask := Pos.double_mask (only parsing).
-Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing).
-Notation Pminus_mask := Pos.sub_mask (only parsing).
-Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
-Notation Pminus := Pos.sub (only parsing).
-Notation Pmult := Pos.mul (only parsing).
-Notation iter_pos := @Pos.iter (only parsing).
-Notation Ppow := Pos.pow (only parsing).
-Notation Pdiv2 := Pos.div2 (only parsing).
-Notation Pdiv2_up := Pos.div2_up (only parsing).
-Notation Psize := Pos.size_nat (only parsing).
-Notation Psize_pos := Pos.size (only parsing).
-Notation Pcompare := Pos.compare_cont (only parsing).
-Notation Plt := Pos.lt (only parsing).
-Notation Pgt := Pos.gt (only parsing).
-Notation Ple := Pos.le (only parsing).
-Notation Pge := Pos.ge (only parsing).
-Notation Pmin := Pos.min (only parsing).
-Notation Pmax := Pos.max (only parsing).
-Notation Peqb := Pos.eqb (only parsing).
-Notation positive_eq_dec := Pos.eq_dec (only parsing).
-Notation xI_succ_xO := Pos.xI_succ_xO (only parsing).
-Notation Psucc_discr := Pos.succ_discr (only parsing).
+
+Notation Psucc := Pos.succ (compat "8.3").
+Notation Pplus := Pos.add (compat "8.3").
+Notation Pplus_carry := Pos.add_carry (compat "8.3").
+Notation Ppred := Pos.pred (compat "8.3").
+Notation Piter_op := Pos.iter_op (compat "8.3").
+Notation Piter_op_succ := Pos.iter_op_succ (compat "8.3").
+Notation Pmult_nat := (Pos.iter_op plus) (compat "8.3").
+Notation nat_of_P := Pos.to_nat (compat "8.3").
+Notation P_of_succ_nat := Pos.of_succ_nat (compat "8.3").
+Notation Pdouble_minus_one := Pos.pred_double (compat "8.3").
+Notation positive_mask := Pos.mask (compat "8.3").
+Notation positive_mask_rect := Pos.mask_rect (compat "8.3").
+Notation positive_mask_ind := Pos.mask_ind (compat "8.3").
+Notation positive_mask_rec := Pos.mask_rec (compat "8.3").
+Notation Pdouble_plus_one_mask := Pos.succ_double_mask (compat "8.3").
+Notation Pdouble_mask := Pos.double_mask (compat "8.3").
+Notation Pdouble_minus_two := Pos.double_pred_mask (compat "8.3").
+Notation Pminus_mask := Pos.sub_mask (compat "8.3").
+Notation Pminus_mask_carry := Pos.sub_mask_carry (compat "8.3").
+Notation Pminus := Pos.sub (compat "8.3").
+Notation Pmult := Pos.mul (compat "8.3").
+Notation iter_pos := @Pos.iter (compat "8.3").
+Notation Ppow := Pos.pow (compat "8.3").
+Notation Pdiv2 := Pos.div2 (compat "8.3").
+Notation Pdiv2_up := Pos.div2_up (compat "8.3").
+Notation Psize := Pos.size_nat (compat "8.3").
+Notation Psize_pos := Pos.size (compat "8.3").
+Notation Pcompare := Pos.compare_cont (compat "8.3").
+Notation Plt := Pos.lt (compat "8.3").
+Notation Pgt := Pos.gt (compat "8.3").
+Notation Ple := Pos.le (compat "8.3").
+Notation Pge := Pos.ge (compat "8.3").
+Notation Pmin := Pos.min (compat "8.3").
+Notation Pmax := Pos.max (compat "8.3").
+Notation Peqb := Pos.eqb (compat "8.3").
+Notation positive_eq_dec := Pos.eq_dec (compat "8.3").
+Notation xI_succ_xO := Pos.xI_succ_xO (compat "8.3").
+Notation Psucc_discr := Pos.succ_discr (compat "8.3").
 Notation Psucc_o_double_minus_one_eq_xO :=
- Pos.succ_pred_double (only parsing).
+ Pos.succ_pred_double (compat "8.3").
 Notation Pdouble_minus_one_o_succ_eq_xI :=
- Pos.pred_double_succ (only parsing).
-Notation xO_succ_permute := Pos.double_succ (only parsing).
+ Pos.pred_double_succ (compat "8.3").
+Notation xO_succ_permute := Pos.double_succ (compat "8.3").
 Notation double_moins_un_xO_discr :=
- Pos.pred_double_xO_discr (only parsing).
-Notation Psucc_not_one := Pos.succ_not_1 (only parsing).
-Notation Ppred_succ := Pos.pred_succ (only parsing).
-Notation Psucc_pred := Pos.succ_pred_or (only parsing).
-Notation Psucc_inj := Pos.succ_inj (only parsing).
-Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing).
-Notation Pplus_comm := Pos.add_comm (only parsing).
-Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing).
-Notation Pplus_succ_permute_l := Pos.add_succ_l (only parsing).
-Notation Pplus_no_neutral := Pos.add_no_neutral (only parsing).
-Notation Pplus_carry_plus := Pos.add_carry_add (only parsing).
-Notation Pplus_reg_r := Pos.add_reg_r (only parsing).
-Notation Pplus_reg_l := Pos.add_reg_l (only parsing).
-Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (only parsing).
-Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (only parsing).
-Notation Pplus_assoc := Pos.add_assoc (only parsing).
-Notation Pplus_xO := Pos.add_xO (only parsing).
-Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (only parsing).
-Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (only parsing).
-Notation Pplus_diag := Pos.add_diag (only parsing).
-Notation PeanoView := Pos.PeanoView (only parsing).
-Notation PeanoOne := Pos.PeanoOne (only parsing).
-Notation PeanoSucc := Pos.PeanoSucc (only parsing).
-Notation PeanoView_rect := Pos.PeanoView_rect (only parsing).
-Notation PeanoView_ind := Pos.PeanoView_ind (only parsing).
-Notation PeanoView_rec := Pos.PeanoView_rec (only parsing).
-Notation peanoView_xO := Pos.peanoView_xO (only parsing).
-Notation peanoView_xI := Pos.peanoView_xI (only parsing).
-Notation peanoView := Pos.peanoView (only parsing).
-Notation PeanoView_iter := Pos.PeanoView_iter (only parsing).
-Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (only parsing).
-Notation PeanoViewUnique := Pos.PeanoViewUnique (only parsing).
-Notation Prect := Pos.peano_rect (only parsing).
-Notation Prect_succ := Pos.peano_rect_succ (only parsing).
-Notation Prect_base := Pos.peano_rect_base (only parsing).
-Notation Prec := Pos.peano_rec (only parsing).
-Notation Pind := Pos.peano_ind (only parsing).
-Notation Pcase := Pos.peano_case (only parsing).
-Notation Pmult_1_r := Pos.mul_1_r (only parsing).
-Notation Pmult_Sn_m := Pos.mul_succ_l (only parsing).
-Notation Pmult_xO_permute_r := Pos.mul_xO_r (only parsing).
-Notation Pmult_xI_permute_r := Pos.mul_xI_r (only parsing).
-Notation Pmult_comm := Pos.mul_comm (only parsing).
-Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (only parsing).
-Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (only parsing).
-Notation Pmult_assoc := Pos.mul_assoc (only parsing).
-Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (only parsing).
-Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing).
-Notation Pmult_reg_r := Pos.mul_reg_r (only parsing).
-Notation Pmult_reg_l := Pos.mul_reg_l (only parsing).
-Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing).
-Notation Psquare_xO := Pos.square_xO (only parsing).
-Notation Psquare_xI := Pos.square_xI (only parsing).
-Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing).
-Notation iter_pos_swap := Pos.iter_swap (only parsing).
-Notation iter_pos_succ := Pos.iter_succ (only parsing).
-Notation iter_pos_plus := Pos.iter_add (only parsing).
-Notation iter_pos_invariant := Pos.iter_invariant (only parsing).
-Notation Ppow_1_r := Pos.pow_1_r (only parsing).
-Notation Ppow_succ_r := Pos.pow_succ_r (only parsing).
-Notation Peqb_refl := Pos.eqb_refl (only parsing).
-Notation Peqb_eq := Pos.eqb_eq (only parsing).
-Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing).
-Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing).
-Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing).
-Notation Pcompare_eq_Lt := Pos.compare_lt_iff (only parsing).
-Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing).
-
-Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing).
-Notation ZC1 := Pos.gt_lt (only parsing).
-Notation ZC2 := Pos.lt_gt (only parsing).
-Notation Pcompare_spec := Pos.compare_spec (only parsing).
-Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing).
-Notation Pcompare_succ_succ := Pos.compare_succ_succ (only parsing).
-Notation Pcompare_1 := Pos.nlt_1_r (only parsing).
-Notation Plt_1 := Pos.nlt_1_r (only parsing).
-Notation Plt_1_succ := Pos.lt_1_succ (only parsing).
-Notation Plt_lt_succ := Pos.lt_lt_succ (only parsing).
-Notation Plt_irrefl := Pos.lt_irrefl (only parsing).
-Notation Plt_trans := Pos.lt_trans (only parsing).
-Notation Plt_ind := Pos.lt_ind (only parsing).
-Notation Ple_lteq := Pos.le_lteq (only parsing).
-Notation Ple_refl := Pos.le_refl (only parsing).
-Notation Ple_lt_trans := Pos.le_lt_trans (only parsing).
-Notation Plt_le_trans := Pos.lt_le_trans (only parsing).
-Notation Ple_trans := Pos.le_trans (only parsing).
-Notation Plt_succ_r := Pos.lt_succ_r (only parsing).
-Notation Ple_succ_l := Pos.le_succ_l (only parsing).
-Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing).
-Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing).
-Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing).
-Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (only parsing).
-Notation Pplus_lt_mono := Pos.add_lt_mono (only parsing).
-Notation Pplus_le_mono_l := Pos.add_le_mono_l (only parsing).
-Notation Pplus_le_mono_r := Pos.add_le_mono_r (only parsing).
-Notation Pplus_le_mono := Pos.add_le_mono (only parsing).
-Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (only parsing).
-Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (only parsing).
-Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (only parsing).
-Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (only parsing).
-Notation Pmult_lt_mono := Pos.mul_lt_mono (only parsing).
-Notation Pmult_le_mono_l := Pos.mul_le_mono_l (only parsing).
-Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing).
-Notation Pmult_le_mono := Pos.mul_le_mono (only parsing).
-Notation Plt_plus_r := Pos.lt_add_r (only parsing).
-Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing).
-Notation Ppow_gt_1 := Pos.pow_gt_1 (only parsing).
-Notation Ppred_mask := Pos.pred_mask (only parsing).
-Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing).
-Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing).
-Notation Pminus_succ_r := Pos.sub_succ_r (only parsing).
-Notation Pminus_mask_diag := Pos.sub_mask_diag (only parsing).
-
-Notation Pplus_minus_eq := Pos.add_sub (only parsing).
-Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (only parsing).
-Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (only parsing).
-Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (only parsing).
-Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (only parsing).
-Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (only parsing).
-Notation Pminus_decr := Pos.sub_decr (only parsing).
-Notation Pminus_xI_xI := Pos.sub_xI_xI (only parsing).
-Notation Pplus_minus_assoc := Pos.add_sub_assoc (only parsing).
-Notation Pminus_plus_distr := Pos.sub_add_distr (only parsing).
-Notation Pminus_minus_distr := Pos.sub_sub_distr (only parsing).
-Notation Pminus_mask_Lt := Pos.sub_mask_neg (only parsing).
-Notation Pminus_Lt := Pos.sub_lt (only parsing).
-Notation Pminus_Eq := Pos.sub_diag (only parsing).
-Notation Psize_monotone := Pos.size_nat_monotone (only parsing).
-Notation Psize_pos_gt := Pos.size_gt (only parsing).
-Notation Psize_pos_le := Pos.size_le (only parsing).
+ Pos.pred_double_xO_discr (compat "8.3").
+Notation Psucc_not_one := Pos.succ_not_1 (compat "8.3").
+Notation Ppred_succ := Pos.pred_succ (compat "8.3").
+Notation Psucc_pred := Pos.succ_pred_or (compat "8.3").
+Notation Psucc_inj := Pos.succ_inj (compat "8.3").
+Notation Pplus_carry_spec := Pos.add_carry_spec (compat "8.3").
+Notation Pplus_comm := Pos.add_comm (compat "8.3").
+Notation Pplus_succ_permute_r := Pos.add_succ_r (compat "8.3").
+Notation Pplus_succ_permute_l := Pos.add_succ_l (compat "8.3").
+Notation Pplus_no_neutral := Pos.add_no_neutral (compat "8.3").
+Notation Pplus_carry_plus := Pos.add_carry_add (compat "8.3").
+Notation Pplus_reg_r := Pos.add_reg_r (compat "8.3").
+Notation Pplus_reg_l := Pos.add_reg_l (compat "8.3").
+Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (compat "8.3").
+Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (compat "8.3").
+Notation Pplus_assoc := Pos.add_assoc (compat "8.3").
+Notation Pplus_xO := Pos.add_xO (compat "8.3").
+Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (compat "8.3").
+Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (compat "8.3").
+Notation Pplus_diag := Pos.add_diag (compat "8.3").
+Notation PeanoView := Pos.PeanoView (compat "8.3").
+Notation PeanoOne := Pos.PeanoOne (compat "8.3").
+Notation PeanoSucc := Pos.PeanoSucc (compat "8.3").
+Notation PeanoView_rect := Pos.PeanoView_rect (compat "8.3").
+Notation PeanoView_ind := Pos.PeanoView_ind (compat "8.3").
+Notation PeanoView_rec := Pos.PeanoView_rec (compat "8.3").
+Notation peanoView_xO := Pos.peanoView_xO (compat "8.3").
+Notation peanoView_xI := Pos.peanoView_xI (compat "8.3").
+Notation peanoView := Pos.peanoView (compat "8.3").
+Notation PeanoView_iter := Pos.PeanoView_iter (compat "8.3").
+Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (compat "8.3").
+Notation PeanoViewUnique := Pos.PeanoViewUnique (compat "8.3").
+Notation Prect := Pos.peano_rect (compat "8.3").
+Notation Prect_succ := Pos.peano_rect_succ (compat "8.3").
+Notation Prect_base := Pos.peano_rect_base (compat "8.3").
+Notation Prec := Pos.peano_rec (compat "8.3").
+Notation Pind := Pos.peano_ind (compat "8.3").
+Notation Pcase := Pos.peano_case (compat "8.3").
+Notation Pmult_1_r := Pos.mul_1_r (compat "8.3").
+Notation Pmult_Sn_m := Pos.mul_succ_l (compat "8.3").
+Notation Pmult_xO_permute_r := Pos.mul_xO_r (compat "8.3").
+Notation Pmult_xI_permute_r := Pos.mul_xI_r (compat "8.3").
+Notation Pmult_comm := Pos.mul_comm (compat "8.3").
+Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (compat "8.3").
+Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (compat "8.3").
+Notation Pmult_assoc := Pos.mul_assoc (compat "8.3").
+Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (compat "8.3").
+Notation Pmult_xO_discr := Pos.mul_xO_discr (compat "8.3").
+Notation Pmult_reg_r := Pos.mul_reg_r (compat "8.3").
+Notation Pmult_reg_l := Pos.mul_reg_l (compat "8.3").
+Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (compat "8.3").
+Notation Psquare_xO := Pos.square_xO (compat "8.3").
+Notation Psquare_xI := Pos.square_xI (compat "8.3").
+Notation iter_pos_swap_gen := Pos.iter_swap_gen (compat "8.3").
+Notation iter_pos_swap := Pos.iter_swap (compat "8.3").
+Notation iter_pos_succ := Pos.iter_succ (compat "8.3").
+Notation iter_pos_plus := Pos.iter_add (compat "8.3").
+Notation iter_pos_invariant := Pos.iter_invariant (compat "8.3").
+Notation Ppow_1_r := Pos.pow_1_r (compat "8.3").
+Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.3").
+Notation Peqb_refl := Pos.eqb_refl (compat "8.3").
+Notation Peqb_eq := Pos.eqb_eq (compat "8.3").
+Notation Pcompare_refl_id := Pos.compare_cont_refl (compat "8.3").
+Notation Pcompare_eq_iff := Pos.compare_eq_iff (compat "8.3").
+Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (compat "8.3").
+Notation Pcompare_eq_Lt := Pos.compare_lt_iff (compat "8.3").
+Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (compat "8.3").
+
+Notation Pcompare_antisym := Pos.compare_cont_antisym (compat "8.3").
+Notation ZC1 := Pos.gt_lt (compat "8.3").
+Notation ZC2 := Pos.lt_gt (compat "8.3").
+Notation Pcompare_spec := Pos.compare_spec (compat "8.3").
+Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (compat "8.3").
+Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.3").
+Notation Pcompare_1 := Pos.nlt_1_r (compat "8.3").
+Notation Plt_1 := Pos.nlt_1_r (compat "8.3").
+Notation Plt_1_succ := Pos.lt_1_succ (compat "8.3").
+Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.3").
+Notation Plt_irrefl := Pos.lt_irrefl (compat "8.3").
+Notation Plt_trans := Pos.lt_trans (compat "8.3").
+Notation Plt_ind := Pos.lt_ind (compat "8.3").
+Notation Ple_lteq := Pos.le_lteq (compat "8.3").
+Notation Ple_refl := Pos.le_refl (compat "8.3").
+Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.3").
+Notation Plt_le_trans := Pos.lt_le_trans (compat "8.3").
+Notation Ple_trans := Pos.le_trans (compat "8.3").
+Notation Plt_succ_r := Pos.lt_succ_r (compat "8.3").
+Notation Ple_succ_l := Pos.le_succ_l (compat "8.3").
+Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (compat "8.3").
+Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (compat "8.3").
+Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (compat "8.3").
+Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (compat "8.3").
+Notation Pplus_lt_mono := Pos.add_lt_mono (compat "8.3").
+Notation Pplus_le_mono_l := Pos.add_le_mono_l (compat "8.3").
+Notation Pplus_le_mono_r := Pos.add_le_mono_r (compat "8.3").
+Notation Pplus_le_mono := Pos.add_le_mono (compat "8.3").
+Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (compat "8.3").
+Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (compat "8.3").
+Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (compat "8.3").
+Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (compat "8.3").
+Notation Pmult_lt_mono := Pos.mul_lt_mono (compat "8.3").
+Notation Pmult_le_mono_l := Pos.mul_le_mono_l (compat "8.3").
+Notation Pmult_le_mono_r := Pos.mul_le_mono_r (compat "8.3").
+Notation Pmult_le_mono := Pos.mul_le_mono (compat "8.3").
+Notation Plt_plus_r := Pos.lt_add_r (compat "8.3").
+Notation Plt_not_plus_l := Pos.lt_not_add_l (compat "8.3").
+Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.3").
+Notation Ppred_mask := Pos.pred_mask (compat "8.3").
+Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (compat "8.3").
+Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (compat "8.3").
+Notation Pminus_succ_r := Pos.sub_succ_r (compat "8.3").
+Notation Pminus_mask_diag := Pos.sub_mask_diag (compat "8.3").
+
+Notation Pplus_minus_eq := Pos.add_sub (compat "8.3").
+Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (compat "8.3").
+Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (compat "8.3").
+Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (compat "8.3").
+Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (compat "8.3").
+Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (compat "8.3").
+Notation Pminus_decr := Pos.sub_decr (compat "8.3").
+Notation Pminus_xI_xI := Pos.sub_xI_xI (compat "8.3").
+Notation Pplus_minus_assoc := Pos.add_sub_assoc (compat "8.3").
+Notation Pminus_plus_distr := Pos.sub_add_distr (compat "8.3").
+Notation Pminus_minus_distr := Pos.sub_sub_distr (compat "8.3").
+Notation Pminus_mask_Lt := Pos.sub_mask_neg (compat "8.3").
+Notation Pminus_Lt := Pos.sub_lt (compat "8.3").
+Notation Pminus_Eq := Pos.sub_diag (compat "8.3").
+Notation Psize_monotone := Pos.size_nat_monotone (compat "8.3").
+Notation Psize_pos_gt := Pos.size_gt (compat "8.3").
+Notation Psize_pos_le := Pos.size_le (compat "8.3").
 
 (** More complex compatibility facts, expressed as lemmas
     (to preserve scopes for instance) *)
@@ -2056,24 +2056,24 @@ Lemma Peqb_true_eq x y : Pos.eqb x y = true -> x=y.
 Proof. apply Pos.eqb_eq. Qed.
 Lemma Pcompare_eq_Gt p q : (p ?= q) = Gt <-> p > q.
 Proof. reflexivity. Qed.
-Lemma Pplus_one_succ_r p : Psucc p = p + 1.
+Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
 Proof (eq_sym (Pos.add_1_r p)).
-Lemma Pplus_one_succ_l p : Psucc p = 1 + p.
+Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p.
 Proof (eq_sym (Pos.add_1_l p)).
-Lemma Pcompare_refl p : Pcompare p p Eq = Eq.
+Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq.
 Proof (Pos.compare_cont_refl p Eq).
-Lemma Pcompare_Eq_eq : forall p q, Pcompare p q Eq = Eq -> p = q.
+Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q.
 Proof Pos.compare_eq.
-Lemma ZC4 p q : Pcompare p q Eq = CompOpp (Pcompare q p Eq).
+Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq).
 Proof (Pos.compare_antisym q p).
-Lemma Ppred_minus p : Ppred p = p - 1.
+Lemma Ppred_minus p : Pos.pred p = p - 1.
 Proof (eq_sym (Pos.sub_1_r p)).
 
 Lemma Pminus_mask_Gt p q :
   p > q ->
   exists h : positive,
-   Pminus_mask p q = IsPos h /\
-   q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
+   Pos.sub_mask p q = IsPos h /\
+   q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = IsPos (Pos.pred h)).
 Proof.
  intros H. apply Pos.gt_lt in H.
  destruct (Pos.sub_mask_pos p q H) as (r & U).
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 7916511a..4beeea31 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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        *)
@@ -288,9 +288,6 @@ Definition max p p' :=
 
 (** ** Boolean equality and comparisons *)
 
-(** Nota: this [eqb] is not convertible with the generated [positive_beq], due
-    to a different guard argument. We keep this version for compatibility. *)
-
 Fixpoint eqb p q {struct q} :=
   match p, q with
     | p~1, q~1 => eqb p q
diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v
index 26b8265b..9d294026 100644
--- a/theories/PArith/PArith.v
+++ b/theories/PArith/PArith.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/PArith/POrderedType.v b/theories/PArith/POrderedType.v
index de7b2b82..4aae6271 100644
--- a/theories/PArith/POrderedType.v
+++ b/theories/PArith/POrderedType.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/PArith/Pnat.v b/theories/PArith/Pnat.v
index f9df70bd..31e88a40 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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        *)
@@ -30,7 +30,7 @@ Qed.
 
 Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q.
 Proof.
- revert q. induction p using Pind; intros q.
+ revert q. induction p using peano_ind; intros q.
  now rewrite add_1_l, inj_succ.
  now rewrite add_succ_l, !inj_succ, IHp.
 Qed.
@@ -378,55 +378,56 @@ End SuccNat2Pos.
 
 (** For compatibility, old names and old-style lemmas *)
 
-Notation Psucc_S := Pos2Nat.inj_succ (only parsing).
-Notation Pplus_plus := Pos2Nat.inj_add (only parsing).
-Notation Pmult_mult := Pos2Nat.inj_mul (only parsing).
-Notation Pcompare_nat_compare := Pos2Nat.inj_compare (only parsing).
-Notation nat_of_P_xH := Pos2Nat.inj_1 (only parsing).
-Notation nat_of_P_xO := Pos2Nat.inj_xO (only parsing).
-Notation nat_of_P_xI := Pos2Nat.inj_xI (only parsing).
-Notation nat_of_P_is_S := Pos2Nat.is_succ (only parsing).
-Notation nat_of_P_pos := Pos2Nat.is_pos (only parsing).
-Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (only parsing).
-Notation nat_of_P_inj := Pos2Nat.inj (only parsing).
-Notation Plt_lt := Pos2Nat.inj_lt (only parsing).
-Notation Pgt_gt := Pos2Nat.inj_gt (only parsing).
-Notation Ple_le := Pos2Nat.inj_le (only parsing).
-Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
-Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
-Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).
-
-Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing).
-Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing).
-
-Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing).
-Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing).
-Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing).
-Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing).
-Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing).
-Notation ZL4 := Pos2Nat.is_succ (only parsing).
-Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing).
-Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing).
-Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing).
+Notation Psucc_S := Pos2Nat.inj_succ (compat "8.3").
+Notation Pplus_plus := Pos2Nat.inj_add (compat "8.3").
+Notation Pmult_mult := Pos2Nat.inj_mul (compat "8.3").
+Notation Pcompare_nat_compare := Pos2Nat.inj_compare (compat "8.3").
+Notation nat_of_P_xH := Pos2Nat.inj_1 (compat "8.3").
+Notation nat_of_P_xO := Pos2Nat.inj_xO (compat "8.3").
+Notation nat_of_P_xI := Pos2Nat.inj_xI (compat "8.3").
+Notation nat_of_P_is_S := Pos2Nat.is_succ (compat "8.3").
+Notation nat_of_P_pos := Pos2Nat.is_pos (compat "8.3").
+Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (compat "8.3").
+Notation nat_of_P_inj := Pos2Nat.inj (compat "8.3").
+Notation Plt_lt := Pos2Nat.inj_lt (compat "8.3").
+Notation Pgt_gt := Pos2Nat.inj_gt (compat "8.3").
+Notation Ple_le := Pos2Nat.inj_le (compat "8.3").
+Notation Pge_ge := Pos2Nat.inj_ge (compat "8.3").
+Notation Pminus_minus := Pos2Nat.inj_sub (compat "8.3").
+Notation iter_nat_of_P := @Pos2Nat.inj_iter (compat "8.3").
+
+Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (compat "8.3").
+Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (compat "8.3").
+
+Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (compat "8.3").
+Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (compat "8.3").
+Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (compat "8.3").
+Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (compat "8.3").
+Notation lt_O_nat_of_P := Pos2Nat.is_pos (compat "8.3").
+Notation ZL4 := Pos2Nat.is_succ (compat "8.3").
+Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (compat "8.3").
+Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3").
+Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3").
 
 Lemma nat_of_P_minus_morphism p q :
- Pcompare p q Eq = Gt -> Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
-Proof (fun H => Pos2Nat.inj_sub p q (ZC1 _ _ H)).
+ Pos.compare_cont p q Eq = Gt ->
+  Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
+Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)).
 
 Lemma nat_of_P_lt_Lt_compare_morphism p q :
- Pcompare p q Eq = Lt -> Pos.to_nat p < Pos.to_nat q.
+ Pos.compare_cont p q Eq = Lt -> Pos.to_nat p < Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_lt p q)).
 
 Lemma nat_of_P_gt_Gt_compare_morphism p q :
- Pcompare p q Eq = Gt -> Pos.to_nat p > Pos.to_nat q.
+ Pos.compare_cont p q Eq = Gt -> Pos.to_nat p > Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_gt p q)).
 
 Lemma nat_of_P_lt_Lt_compare_complement_morphism p q :
- Pos.to_nat p < Pos.to_nat q -> Pcompare p q Eq = Lt.
+ Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont p q Eq = Lt.
 Proof (proj2 (Pos2Nat.inj_lt p q)).
 
 Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
- Pos.to_nat p > Pos.to_nat q -> Pcompare p q Eq = Gt.
+ Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont p q Eq = Gt.
 Proof (proj2 (Pos2Nat.inj_gt p q)).
 
 (** Old intermediate results about [Pmult_nat] *)
@@ -445,7 +446,7 @@ Proof.
 Qed.
 
 Lemma Pmult_nat_succ_morphism :
- forall p n, Pmult_nat (Psucc p) n = n + Pmult_nat p n.
+ forall p n, Pmult_nat (Pos.succ p) n = n + Pmult_nat p n.
 Proof.
  intros. now rewrite !Pmult_nat_mult, Pos2Nat.inj_succ.
 Qed.
@@ -457,7 +458,7 @@ Proof.
 Qed.
 
 Theorem Pmult_nat_plus_carry_morphism :
- forall p q n, Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.
+ forall p q n, Pmult_nat (Pos.add_carry p q) n = n + Pmult_nat (p + q) n.
 Proof.
  intros. now rewrite Pos.add_carry_spec, Pmult_nat_succ_morphism.
 Qed.