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.

5 files changed, 44 insertions, 44 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 22e10e2e4..84ec90785 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -359,14 +359,14 @@ Definition idProp : IDProp := fun A x => x.
 
 (* Compatibility *)
 
-Notation prodT := prod (compat "8.2").
-Notation pairT := pair (compat "8.2").
-Notation prodT_rect := prod_rect (compat "8.2").
-Notation prodT_rec := prod_rec (compat "8.2").
-Notation prodT_ind := prod_ind (compat "8.2").
-Notation fstT := fst (compat "8.2").
-Notation sndT := snd (compat "8.2").
-Notation prodT_uncurry := prod_uncurry (compat "8.2").
-Notation prodT_curry := prod_curry (compat "8.2").
+Notation prodT := prod (only parsing).
+Notation pairT := pair (only parsing).
+Notation prodT_rect := prod_rect (only parsing).
+Notation prodT_rec := prod_rec (only parsing).
+Notation prodT_ind := prod_ind (only parsing).
+Notation fstT := fst (only parsing).
+Notation sndT := snd (only parsing).
+Notation prodT_uncurry := prod_uncurry (only parsing).
+Notation prodT_curry := prod_curry (only parsing).
 
 (* end hide *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 053ed601f..2209d13ff 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -549,14 +549,14 @@ Qed.
 
 (* Aliases *)
 
-Notation sym_eq := eq_sym (compat "8.3").
-Notation trans_eq := eq_trans (compat "8.3").
-Notation sym_not_eq := not_eq_sym (compat "8.3").
-
-Notation refl_equal := eq_refl (compat "8.3").
-Notation sym_equal := eq_sym (compat "8.3").
-Notation trans_equal := eq_trans (compat "8.3").
-Notation sym_not_equal := not_eq_sym (compat "8.3").
+Notation sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := not_eq_sym (only parsing).
+
+Notation refl_equal := eq_refl (only parsing).
+Notation sym_equal := eq_sym (only parsing).
+Notation trans_equal := eq_trans (only parsing).
+Notation sym_not_equal := not_eq_sym (only parsing).
 
 Hint Immediate eq_sym not_eq_sym: core.
 
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 567d2c15c..3244fa14c 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -66,7 +66,7 @@ Defined.
 
 Hint Immediate identity_sym not_identity_sym: core.
 
-Notation refl_id := identity_refl (compat "8.3").
-Notation sym_id := identity_sym (compat "8.3").
-Notation trans_id := identity_trans (compat "8.3").
-Notation sym_not_id := not_identity_sym (compat "8.3").
+Notation refl_id := identity_refl (only parsing).
+Notation sym_id := identity_sym (only parsing).
+Notation trans_id := identity_trans (only parsing).
+Notation sym_not_id := not_identity_sym (only parsing).
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.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 47e8a7558..e9d6a1597 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -742,16 +742,16 @@ Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
-Notation sigS := sigT (compat "8.2").
-Notation existS := existT (compat "8.2").
-Notation sigS_rect := sigT_rect (compat "8.2").
-Notation sigS_rec := sigT_rec (compat "8.2").
-Notation sigS_ind := sigT_ind (compat "8.2").
-Notation projS1 := projT1 (compat "8.2").
-Notation projS2 := projT2 (compat "8.2").
-
-Notation sigS2 := sigT2 (compat "8.2").
-Notation existS2 := existT2 (compat "8.2").
-Notation sigS2_rect := sigT2_rect (compat "8.2").
-Notation sigS2_rec := sigT2_rec (compat "8.2").
-Notation sigS2_ind := sigT2_ind (compat "8.2").
+Notation sigS := sigT (compat "8.6").
+Notation existS := existT (compat "8.6").
+Notation sigS_rect := sigT_rect (compat "8.6").
+Notation sigS_rec := sigT_rec (compat "8.6").
+Notation sigS_ind := sigT_ind (compat "8.6").
+Notation projS1 := projT1 (compat "8.6").
+Notation projS2 := projT2 (compat "8.6").
+
+Notation sigS2 := sigT2 (compat "8.6").
+Notation existS2 := existT2 (compat "8.6").
+Notation sigS2_rect := sigT2_rect (compat "8.6").
+Notation sigS2_rec := sigT2_rec (compat "8.6").
+Notation sigS2_ind := sigT2_ind (compat "8.6").