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/Arith/Compare_dec.v | 12 ++++++------ theories/Arith/Div2.v | 4 ++-- theories/Arith/EqNat.v | 6 +++--- theories/Arith/Le.v | 18 +++++++++--------- theories/Arith/Lt.v | 24 ++++++++++++------------ theories/Arith/Minus.v | 10 +++++----- theories/Arith/Mult.v | 24 ++++++++++++------------ theories/Arith/Peano_dec.v | 2 +- theories/Arith/Plus.v | 12 ++++++------ 9 files changed, 56 insertions(+), 56 deletions(-) (limited to 'theories/Arith') 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 (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 -> 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 *) -- cgit v1.2.3