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

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. *)