1 files changed, 10 insertions, 10 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 571d2f2dd..857913c3e 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -37,7 +37,7 @@ Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
 
-Notation pred := Nat.pred (compat "8.4").
+Notation pred := Nat.pred (only parsing).
 
 Definition f_equal_pred := f_equal pred.
 
@@ -79,7 +79,7 @@ Hint Resolve n_Sn: core.
 
 (** Addition *)
 
-Notation plus := Nat.add (compat "8.4").
+Notation plus := Nat.add (only parsing).
 Infix "+" := Nat.add : nat_scope.
 
 Definition f_equal2_plus := f_equal2 plus.
@@ -110,12 +110,12 @@ Qed.
 
 (** Standard associated names *)
 
-Notation plus_0_r_reverse := plus_n_O (compat "8.2").
-Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2").
+Notation plus_0_r_reverse := plus_n_O (only parsing).
+Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
 
 (** Multiplication *)
 
-Notation mult := Nat.mul (compat "8.4").
+Notation mult := Nat.mul (only parsing).
 Infix "*" := Nat.mul : nat_scope.
 
 Definition f_equal2_mult := f_equal2 mult.
@@ -137,12 +137,12 @@ Hint Resolve mult_n_Sm: core.
 
 (** Standard associated names *)
 
-Notation mult_0_r_reverse := mult_n_O (compat "8.2").
-Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2").
+Notation mult_0_r_reverse := mult_n_O (only parsing).
+Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
 
 (** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
-Notation minus := Nat.sub (compat "8.4").
+Notation minus := Nat.sub (only parsing).
 Infix "-" := Nat.sub : nat_scope.
 
 (** Definition of the usual orders, the basic properties of [le] and [lt]
@@ -219,8 +219,8 @@ Qed.
 
 (** Maximum and minimum : definitions and specifications *)
 
-Notation max := Nat.max (compat "8.4").
-Notation min := Nat.min (compat "8.4").
+Notation max := Nat.max (only parsing).
+Notation min := Nat.min (only parsing).
 
 Lemma max_l n m : m <= n -> Nat.max n m = n.
 Proof.