Remove the deprecation for some 8.2-8.5 compatibility aliases.

This was decided during the Fall WG (2017).

The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.

We change the compat version to 8.6 to allow the removal of VOld and V8_5.

9 files changed, 56 insertions, 56 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 1e3237d10..b7235b669 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -133,11 +133,11 @@ Qed.
     See now [Nat.compare] and its properties.
     In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Notation nat_compare := Nat.compare (compat "8.4").
+Notation nat_compare := Nat.compare (compat "8.6").
 
-Notation nat_compare_spec := Nat.compare_spec (compat "8.4").
-Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4").
-Notation nat_compare_S := Nat.compare_succ (compat "8.4").
+Notation nat_compare_spec := Nat.compare_spec (compat "8.6").
+Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6").
+Notation nat_compare_S := Nat.compare_succ (only parsing).
 
 Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
 Proof.
@@ -198,9 +198,9 @@ Qed.
     See now [Nat.leb] and its properties.
     In scope [nat_scope], the notation for [Nat.leb] is "<=?" *)
 
-Notation leb := Nat.leb (compat "8.4").
+Notation leb := Nat.leb (only parsing).
 
-Notation leb_iff := Nat.leb_le (compat "8.4").
+Notation leb_iff := Nat.leb_le (only parsing).
 
 Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n.
 Proof.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index ecb9a5706..725d65d82 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -18,7 +18,7 @@ Implicit Type n : nat.
 
 (** Here we define [n/2] and prove some of its properties *)
 
-Notation div2 := Nat.div2 (compat "8.4").
+Notation div2 := Nat.div2 (only parsing).
 
 (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
     useful to prove the corresponding induction principle *)
@@ -84,7 +84,7 @@ Qed.
 
 (** Properties related to the double ([2n]) *)
 
-Notation double := Nat.double (compat "8.4").
+Notation double := Nat.double (only parsing).
 
 Hint Unfold double Nat.double: arith.
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 722615428..a4f2d30bd 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -69,10 +69,10 @@ Defined.
    We reuse the one already defined in module [Nat].
    In scope [nat_scope], the notation "=?" can be used. *)
 
-Notation beq_nat := Nat.eqb (compat "8.4").
+Notation beq_nat := Nat.eqb (only parsing).
 
-Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4").
-Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4").
+Notation beq_nat_true_iff := Nat.eqb_eq (only parsing).
+Notation beq_nat_false_iff := Nat.eqb_neq (only parsing).
 
 Lemma beq_nat_refl n : true = (n =? n).
 Proof.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index d95b05770..9fcce4520 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -26,17 +26,17 @@ Local Open Scope nat_scope.
 
 (** * [le] is an order on [nat] *)
 
-Notation le_refl := Nat.le_refl (compat "8.4").
-Notation le_trans := Nat.le_trans (compat "8.4").
-Notation le_antisym := Nat.le_antisymm (compat "8.4").
+Notation le_refl := Nat.le_refl (only parsing).
+Notation le_trans := Nat.le_trans (only parsing).
+Notation le_antisym := Nat.le_antisymm (only parsing).
 
 Hint Resolve le_trans: arith.
 Hint Immediate le_antisym: arith.
 
 (** * Properties of [le] w.r.t 0 *)
 
-Notation le_0_n := Nat.le_0_l (compat "8.4").  (* 0 <= n *)
-Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4").  (* ~ S n <= 0 *)
+Notation le_0_n := Nat.le_0_l (only parsing).  (* 0 <= n *)
+Notation le_Sn_0 := Nat.nle_succ_0 (only parsing).  (* ~ S n <= 0 *)
 
 Lemma le_n_0_eq n : n <= 0 -> 0 = n.
 Proof.
@@ -53,8 +53,8 @@ Proof Peano.le_n_S.
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
 Proof Peano.le_S_n.
 
-Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *)
-Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *)
+Notation le_n_Sn := Nat.le_succ_diag_r (only parsing). (* n <= S n *)
+Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *)
 
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
 Proof Nat.lt_le_incl.
@@ -65,8 +65,8 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 
 (** * Properties of [le] w.r.t predecessor *)
 
-Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *)
-Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *)
+Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *)
+Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *)
 
 Hint Resolve le_pred_n: arith.
 
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 2c2bea4a6..7c3badce1 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -23,7 +23,7 @@ Local Open Scope nat_scope.
 
 (** * Irreflexivity *)
 
-Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *)
+Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *)
 
 Hint Resolve lt_irrefl: arith.
 
@@ -62,12 +62,12 @@ Hint Immediate le_not_lt lt_not_le: arith.
 
 (** * Asymmetry *)
 
-Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *)
+Notation lt_asym := Nat.lt_asymm (only parsing). (* n<m -> ~m<n *)
 
 (** * Order and 0 *)
 
-Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *)
-Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *)
+Notation lt_0_Sn := Nat.lt_0_succ (only parsing). (* 0 < S n *)
+Notation lt_n_0 := Nat.nlt_0_r (only parsing). (* ~ n < 0 *)
 
 Theorem neq_0_lt n : 0 <> n -> 0 < n.
 Proof.
@@ -84,8 +84,8 @@ Hint Immediate neq_0_lt lt_0_neq: arith.
 
 (** * Order and successor *)
 
-Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *)
-Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *)
+Notation lt_n_Sn := Nat.lt_succ_diag_r (only parsing). (* n < S n *)
+Notation lt_S := Nat.lt_lt_succ_r (only parsing). (* n < m -> n < S m *)
 
 Theorem lt_n_S n m : n < m -> S n < S m.
 Proof.
@@ -127,28 +127,28 @@ Hint Resolve lt_pred_n_n: arith.
 
 (** * Transitivity properties *)
 
-Notation lt_trans := Nat.lt_trans (compat "8.4").
-Notation lt_le_trans := Nat.lt_le_trans (compat "8.4").
-Notation le_lt_trans := Nat.le_lt_trans (compat "8.4").
+Notation lt_trans := Nat.lt_trans (only parsing).
+Notation lt_le_trans := Nat.lt_le_trans (only parsing).
+Notation le_lt_trans := Nat.le_lt_trans (only parsing).
 
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.
 
 (** * Large = strict or equal *)
 
-Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4").
+Notation le_lt_or_eq_iff := Nat.lt_eq_cases (only parsing).
 
 Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
  apply Nat.lt_eq_cases.
 Qed.
 
-Notation lt_le_weak := Nat.lt_le_incl (compat "8.4").
+Notation lt_le_weak := Nat.lt_le_incl (only parsing).
 
 Hint Immediate lt_le_weak: arith.
 
 (** * Dichotomy *)
 
-Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *)
+Notation le_or_lt := Nat.le_gt_cases (only parsing). (* n <= m \/ m < n *)
 
 Theorem nat_total_order n m : n <> m -> n < m \/ m < n.
 Proof.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 950f985d4..ffa1e048c 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -46,7 +46,7 @@ Qed.
 
 (** * Diagonal *)
 
-Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *)
+Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *)
 
 Lemma minus_diag_reverse n : 0 = n - n.
 Proof.
@@ -87,13 +87,13 @@ Qed.
 (** * Relation with order *)
 
 Notation minus_le_compat_r :=
-  Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *)
+  Nat.sub_le_mono_r (only parsing). (* n <= m -> n - p <= m - p. *)
 
 Notation minus_le_compat_l :=
-  Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *)
+  Nat.sub_le_mono_l (only parsing). (* n <= m -> p - m <= p - n. *)
 
-Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *)
-Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *)
+Notation le_minus := Nat.le_sub_l (only parsing). (* n - m <= n *)
+Notation lt_minus := Nat.sub_lt (only parsing). (* m <= n -> 0 < m -> n-m < n *)
 
 Lemma lt_O_minus_lt n m : 0 < n - m -> m < n.
 Proof.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index e4084ba47..4b13e145a 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -23,35 +23,35 @@ Local Open Scope nat_scope.
 
 (** ** Zero property *)
 
-Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *)
-Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *)
+Notation mult_0_l := Nat.mul_0_l (only parsing). (* 0 * n = 0 *)
+Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *)
 
 (** ** 1 is neutral *)
 
-Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *)
-Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *)
+Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *)
+Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *)
 
 Hint Resolve mult_1_l mult_1_r: arith.
 
 (** ** Commutativity *)
 
-Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *)
+Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *)
 
 Hint Resolve mult_comm: arith.
 
 (** ** Distributivity *)
 
 Notation mult_plus_distr_r :=
-  Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *)
+  Nat.mul_add_distr_r (only parsing). (* (n+m)*p = n*p + m*p *)
 
 Notation mult_plus_distr_l :=
-  Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *)
+  Nat.mul_add_distr_l (only parsing). (* n*(m+p) = n*m + n*p *)
 
 Notation mult_minus_distr_r :=
-  Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *)
+  Nat.mul_sub_distr_r (only parsing). (* (n-m)*p = n*p - m*p *)
 
 Notation mult_minus_distr_l :=
-  Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *)
+  Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *)
 
 Hint Resolve mult_plus_distr_r: arith.
 Hint Resolve mult_minus_distr_r: arith.
@@ -59,7 +59,7 @@ Hint Resolve mult_minus_distr_l: arith.
 
 (** ** Associativity *)
 
-Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *)
+Notation mult_assoc := Nat.mul_assoc (only parsing). (* n*(m*p)=n*m*p *)
 
 Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p).
 Proof.
@@ -83,8 +83,8 @@ Qed.
 
 (** ** Multiplication and successor *)
 
-Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *)
-Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *)
+Notation mult_succ_l := Nat.mul_succ_l (only parsing). (* S n * m = n * m + m *)
+Notation mult_succ_r := Nat.mul_succ_r (only parsing). (* n * S m = n * m + n *)
 
 (** * Compatibility with orders *)
 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 247ea20a8..9ed08f1b1 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -19,7 +19,7 @@ Proof.
   - left; exists n; auto.
 Defined.
 
-Notation eq_nat_dec := Nat.eq_dec (compat "8.4").
+Notation eq_nat_dec := Nat.eq_dec (only parsing).
 
 Hint Resolve O_or_S eq_nat_dec: arith.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 600e5e518..3e44bbfe5 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -27,12 +27,12 @@ Local Open Scope nat_scope.
 
 (** * Neutrality of 0, commutativity, associativity *)
 
-Notation plus_0_l := Nat.add_0_l (compat "8.4").
-Notation plus_0_r := Nat.add_0_r (compat "8.4").
-Notation plus_comm := Nat.add_comm (compat "8.4").
-Notation plus_assoc := Nat.add_assoc (compat "8.4").
+Notation plus_0_l := Nat.add_0_l (only parsing).
+Notation plus_0_r := Nat.add_0_r (only parsing).
+Notation plus_comm := Nat.add_comm (only parsing).
+Notation plus_assoc := Nat.add_assoc (only parsing).
 
-Notation plus_permute := Nat.add_shuffle3 (compat "8.4").
+Notation plus_permute := Nat.add_shuffle3 (only parsing).
 
 Definition plus_Snm_nSm : forall n m, S n + m = n + S m :=
  Peano.plus_n_Sm.
@@ -138,7 +138,7 @@ Defined.
 
 (** * Derived properties *)
 
-Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4").
+Notation plus_permute_2_in_4 := Nat.add_shuffle1 (only parsing).
 
 (** * Tail-recursive plus *)