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, 31 insertions, 31 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 814b67322..00019b1a3 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -25,20 +25,20 @@ Open Scope Z_scope.
      - properties of the efficient [Z.gcd] function
 *)
 
-Notation Zgcd := Z.gcd (only parsing).
-Notation Zggcd := Z.ggcd (only parsing).
-Notation Zggcd_gcd := Z.ggcd_gcd (only parsing).
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing).
-Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing).
-Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing).
-Notation Zgcd_greatest := Z.gcd_greatest (only parsing).
-Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing).
-Notation Zggcd_opp := Z.ggcd_opp (only parsing).
+Notation Zgcd := Z.gcd (compat "8.3").
+Notation Zggcd := Z.ggcd (compat "8.3").
+Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3").
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3").
+Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3").
+Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3").
+Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3").
+Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3").
+Notation Zggcd_opp := Z.ggcd_opp (compat "8.3").
 
 (** The former specialized inductive predicate [Zdivide] is now
     a generic existential predicate. *)
 
-Notation Zdivide := Z.divide (only parsing).
+Notation Zdivide := Z.divide (compat "8.3").
 
 (** Its former constructor is now a pseudo-constructor. *)
 
@@ -46,17 +46,17 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.
 
 (** Results concerning divisibility*)
 
-Notation Zdivide_refl := Z.divide_refl (only parsing).
-Notation Zone_divide := Z.divide_1_l (only parsing).
-Notation Zdivide_0 := Z.divide_0_r (only parsing).
-Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
-Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing).
-Notation Zdivide_plus_r := Z.divide_add_r (only parsing).
-Notation Zdivide_minus_l := Z.divide_sub_r (only parsing).
-Notation Zdivide_mult_l := Z.divide_mul_l (only parsing).
-Notation Zdivide_mult_r := Z.divide_mul_r (only parsing).
-Notation Zdivide_factor_r := Z.divide_factor_l (only parsing).
-Notation Zdivide_factor_l := Z.divide_factor_r (only parsing).
+Notation Zdivide_refl := Z.divide_refl (compat "8.3").
+Notation Zone_divide := Z.divide_1_l (compat "8.3").
+Notation Zdivide_0 := Z.divide_0_r (compat "8.3").
+Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3").
+Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3").
+Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3").
+Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3").
+Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3").
+Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3").
+Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3").
+Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3").
 
 Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).
 Proof. apply Z.divide_opp_r. Qed.
@@ -91,12 +91,12 @@ Qed.
 
 (** Only [1] and [-1] divide [1]. *)
 
-Notation Zdivide_1 := Z.divide_1_r (only parsing).
+Notation Zdivide_1 := Z.divide_1_r (compat "8.3").
 
 (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
 
-Notation Zdivide_antisym := Z.divide_antisym (only parsing).
-Notation Zdivide_trans := Z.divide_trans (only parsing).
+Notation Zdivide_antisym := Z.divide_antisym (compat "8.3").
+Notation Zdivide_trans := Z.divide_trans (compat "8.3").
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
@@ -742,7 +742,7 @@ Qed.
 (** we now prove that [Z.gcd] is indeed a gcd in
    the sense of [Zis_gcd]. *)
 
-Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing).
+Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3").
 
 Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).
 Proof.
@@ -775,8 +775,8 @@ Proof.
   subst. now case (Z.gcd a b).
 Qed.
 
-Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing).
-Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing).
+Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3").
+Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3").
 
 Theorem Zgcd_div_swap0 : forall a b : Z,
  0 < Z.gcd a b ->
@@ -806,16 +806,16 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Notation Zgcd_comm := Z.gcd_comm (only parsing).
+Notation Zgcd_comm := Z.gcd_comm (compat "8.3").
 
 Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
 Proof.
  symmetry. apply Z.gcd_assoc.
 Qed.
 
-Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
-Notation Zgcd_0 := Z.gcd_0_r (only parsing).
-Notation Zgcd_1 := Z.gcd_1_r (only parsing).
+Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3").
+Notation Zgcd_0 := Z.gcd_0_r (compat "8.3").
+Notation Zgcd_1 := Z.gcd_1_r (compat "8.3").
 
 Hint Resolve Zgcd_0 Zgcd_1 : zarith.