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

1 files changed, 81 insertions, 81 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index f3f7b850e..0f709d686 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1375,87 +1375,87 @@ Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope.
 
 (** Compatibility Notations *)
 
-Notation Zdouble_plus_one := Z.succ_double (only parsing).
-Notation Zdouble_minus_one := Z.pred_double (only parsing).
-Notation Zdouble := Z.double (only parsing).
-Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (only parsing).
-Notation Zpred' := Z.pred (only parsing).
-Notation Zplus' := Z.add (only parsing).
-Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
-Notation Zopp := Z.opp (only parsing).
-Notation Zsucc := Z.succ (only parsing).
-Notation Zpred := Z.pred (only parsing).
-Notation Zminus := Z.sub (only parsing).
-Notation Zmult := Z.mul (only parsing).
-Notation Zcompare := Z.compare (only parsing).
-Notation Zsgn := Z.sgn (only parsing).
-Notation Zle := Z.le (only parsing).
-Notation Zge := Z.ge (only parsing).
-Notation Zlt := Z.lt (only parsing).
-Notation Zgt := Z.gt (only parsing).
-Notation Zmax := Z.max (only parsing).
-Notation Zmin := Z.min (only parsing).
-Notation Zabs := Z.abs (only parsing).
-Notation Zabs_nat := Z.abs_nat (only parsing).
-Notation Zabs_N := Z.abs_N (only parsing).
-Notation Z_of_nat := Z.of_nat (only parsing).
-Notation Z_of_N := Z.of_N (only parsing).
-
-Notation Zind := Z.peano_ind (only parsing).
-Notation Zopp_0 := Z.opp_0 (only parsing).
-Notation Zopp_neg := Z.opp_Zneg (only parsing).
-Notation Zopp_involutive := Z.opp_involutive (only parsing).
-Notation Zopp_inj := Z.opp_inj (only parsing).
-Notation Zplus_0_l := Z.add_0_l (only parsing).
-Notation Zplus_0_r := Z.add_0_r (only parsing).
-Notation Zplus_comm := Z.add_comm (only parsing).
-Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
-Notation Zopp_succ := Z.opp_succ (only parsing).
-Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
-Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
-Notation Zplus_assoc := Z.add_assoc (only parsing).
-Notation Zplus_permute := Z.add_shuffle3 (only parsing).
-Notation Zplus_reg_l := Z.add_reg_l (only parsing).
-Notation Zplus_succ_l := Z.add_succ_l (only parsing).
-Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
-Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
-Notation Zsucc_inj := Z.succ_inj (only parsing).
-Notation Zsucc'_inj := Z.succ_inj (only parsing).
-Notation Zsucc'_pred' := Z.succ_pred (only parsing).
-Notation Zpred'_succ' := Z.pred_succ (only parsing).
-Notation Zpred'_inj := Z.pred_inj (only parsing).
-Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
-Notation Zminus_0_r := Z.sub_0_r (only parsing).
-Notation Zminus_diag := Z.sub_diag (only parsing).
-Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
-Notation Zminus_succ_r := Z.sub_succ_r (only parsing).
-Notation Zminus_plus := Z.add_simpl_l (only parsing).
-Notation Zmult_0_l := Z.mul_0_l (only parsing).
-Notation Zmult_0_r := Z.mul_0_r (only parsing).
-Notation Zmult_1_l := Z.mul_1_l (only parsing).
-Notation Zmult_1_r := Z.mul_1_r (only parsing).
-Notation Zmult_comm := Z.mul_comm (only parsing).
-Notation Zmult_assoc := Z.mul_assoc (only parsing).
-Notation Zmult_permute := Z.mul_shuffle3 (only parsing).
-Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing).
-Notation Zdouble_mult := Z.double_spec (only parsing).
-Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing).
-Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing).
-Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing).
-Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing).
-Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing).
-Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing).
-Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing).
-Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing).
-Notation Zmult_reg_l := Z.mul_reg_l (only parsing).
-Notation Zmult_reg_r := Z.mul_reg_r (only parsing).
-Notation Zmult_succ_l := Z.mul_succ_l (only parsing).
-Notation Zmult_succ_r := Z.mul_succ_r (only parsing).
-Notation Zpos_xI := Z.pos_xI (only parsing).
-Notation Zpos_xO := Z.pos_xO (only parsing).
-Notation Zneg_xI := Z.neg_xI (only parsing).
-Notation Zneg_xO := Z.neg_xO (only parsing).
+Notation Zdouble_plus_one := Z.succ_double (compat "8.3").
+Notation Zdouble_minus_one := Z.pred_double (compat "8.3").
+Notation Zdouble := Z.double (compat "8.3").
+Notation ZPminus := Z.pos_sub (compat "8.3").
+Notation Zsucc' := Z.succ (compat "8.3").
+Notation Zpred' := Z.pred (compat "8.3").
+Notation Zplus' := Z.add (compat "8.3").
+Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *)
+Notation Zopp := Z.opp (compat "8.3").
+Notation Zsucc := Z.succ (compat "8.3").
+Notation Zpred := Z.pred (compat "8.3").
+Notation Zminus := Z.sub (compat "8.3").
+Notation Zmult := Z.mul (compat "8.3").
+Notation Zcompare := Z.compare (compat "8.3").
+Notation Zsgn := Z.sgn (compat "8.3").
+Notation Zle := Z.le (compat "8.3").
+Notation Zge := Z.ge (compat "8.3").
+Notation Zlt := Z.lt (compat "8.3").
+Notation Zgt := Z.gt (compat "8.3").
+Notation Zmax := Z.max (compat "8.3").
+Notation Zmin := Z.min (compat "8.3").
+Notation Zabs := Z.abs (compat "8.3").
+Notation Zabs_nat := Z.abs_nat (compat "8.3").
+Notation Zabs_N := Z.abs_N (compat "8.3").
+Notation Z_of_nat := Z.of_nat (compat "8.3").
+Notation Z_of_N := Z.of_N (compat "8.3").
+
+Notation Zind := Z.peano_ind (compat "8.3").
+Notation Zopp_0 := Z.opp_0 (compat "8.3").
+Notation Zopp_neg := Z.opp_Zneg (compat "8.3").
+Notation Zopp_involutive := Z.opp_involutive (compat "8.3").
+Notation Zopp_inj := Z.opp_inj (compat "8.3").
+Notation Zplus_0_l := Z.add_0_l (compat "8.3").
+Notation Zplus_0_r := Z.add_0_r (compat "8.3").
+Notation Zplus_comm := Z.add_comm (compat "8.3").
+Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3").
+Notation Zopp_succ := Z.opp_succ (compat "8.3").
+Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3").
+Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3").
+Notation Zplus_assoc := Z.add_assoc (compat "8.3").
+Notation Zplus_permute := Z.add_shuffle3 (compat "8.3").
+Notation Zplus_reg_l := Z.add_reg_l (compat "8.3").
+Notation Zplus_succ_l := Z.add_succ_l (compat "8.3").
+Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3").
+Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3").
+Notation Zsucc_inj := Z.succ_inj (compat "8.3").
+Notation Zsucc'_inj := Z.succ_inj (compat "8.3").
+Notation Zsucc'_pred' := Z.succ_pred (compat "8.3").
+Notation Zpred'_succ' := Z.pred_succ (compat "8.3").
+Notation Zpred'_inj := Z.pred_inj (compat "8.3").
+Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3").
+Notation Zminus_0_r := Z.sub_0_r (compat "8.3").
+Notation Zminus_diag := Z.sub_diag (compat "8.3").
+Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3").
+Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3").
+Notation Zminus_plus := Z.add_simpl_l (compat "8.3").
+Notation Zmult_0_l := Z.mul_0_l (compat "8.3").
+Notation Zmult_0_r := Z.mul_0_r (compat "8.3").
+Notation Zmult_1_l := Z.mul_1_l (compat "8.3").
+Notation Zmult_1_r := Z.mul_1_r (compat "8.3").
+Notation Zmult_comm := Z.mul_comm (compat "8.3").
+Notation Zmult_assoc := Z.mul_assoc (compat "8.3").
+Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3").
+Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3").
+Notation Zdouble_mult := Z.double_spec (compat "8.3").
+Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3").
+Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3").
+Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3").
+Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3").
+Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3").
+Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3").
+Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3").
+Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3").
+Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3").
+Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3").
+Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3").
+Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3").
+Notation Zpos_xI := Z.pos_xI (compat "8.3").
+Notation Zpos_xO := Z.pos_xO (compat "8.3").
+Notation Zneg_xI := Z.neg_xI (compat "8.3").
+Notation Zneg_xO := Z.neg_xO (compat "8.3").
 
 Notation Z := Z (only parsing).
 Notation Z_rect := Z_rect (only parsing).