From 406f98b0efed0b5ed0c680c8a747b307d50c8ff4 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 20 Feb 2018 15:17:00 +0100 Subject: 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. --- theories/Init/Datatypes.v | 18 +++++++++--------- theories/Init/Logic.v | 16 ++++++++-------- theories/Init/Logic_Type.v | 8 ++++---- theories/Init/Peano.v | 20 ++++++++++---------- theories/Init/Specif.v | 26 +++++++++++++------------- 5 files changed, 44 insertions(+), 44 deletions(-) (limited to 'theories/Init') 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"). -- cgit v1.2.3