diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:55:59 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:55:59 +0000 |
commit | f93f073df630bb46ddd07802026c0326dc72dafd (patch) | |
tree | 35035375b5c6260ce6f89ccfbbf95a140e562005 /theories/PArith | |
parent | d655986bc6d54c320a6ddd642cefde4a7f3088a9 (diff) |
Notation: a new annotation "compat 8.x" extending "only parsing"
Suppose we declare : Notation foo := bar (compat "8.3").
Then each time foo is used in a script :
- By default nothing particular happens (for the moment)
- But we could get a warning explaining that
"foo is bar since coq > 8.3".
For that, either use the command-line option -verb-compat-notations
or the interactive command "Set Verbose Compat Notations".
- There is also a strict mode, where foo is forbidden : the previous
warning is now an error.
For that, either use the command-line option -no-compat-notations
or the interactive command "Unset Compat Notations".
When Coq is launched in compatibility mode (via -compat 8.x),
using a notation tagged "8.x" will never trigger a warning or error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/PArith')
-rw-r--r-- | theories/PArith/BinPos.v | 348 | ||||
-rw-r--r-- | theories/PArith/Pnat.v | 60 |
2 files changed, 204 insertions, 204 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 2e4d52a29..e22cac7be 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,183 +1871,183 @@ 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 IsNul := Pos.IsNul (compat "8.3"). +Notation IsPos := Pos.IsPos (compat "8.3"). +Notation IsNeg := Pos.IsNeg (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) *) diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index f9df70bd3..0fa6972b7 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -378,36 +378,36 @@ 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. |