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

5 files changed, 134 insertions, 134 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 30e35f501..6128b9740 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -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 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/Ndigits.v b/theories/NArith/Ndigits.v
index b0c335957..06f47d719 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -15,17 +15,17 @@ 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 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 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 (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]. *)
@@ -247,7 +247,7 @@ 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.
@@ -493,7 +493,7 @@ 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. *)
 
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 559f01f16..21f15f976 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -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/Nnat.v b/theories/NArith/Nnat.v
index 133d4c23b..eb8d5961b 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -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 edb6b2895..1375f2803 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -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").