1 files changed, 10 insertions, 10 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 72cca2439..73c8c5ef4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -39,7 +39,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.
 
@@ -81,7 +81,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.
@@ -112,12 +112,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.
@@ -139,12 +139,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]
@@ -221,8 +221,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.