diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-20 15:17:00 +0100 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-02 23:45:44 +0100 |
commit | 406f98b0efed0b5ed0c680c8a747b307d50c8ff4 (patch) | |
tree | 1629ac0aa97c5343c644fddcab9498a2afc76998 /theories/Arith/Lt.v | |
parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) |
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.
Diffstat (limited to 'theories/Arith/Lt.v')
-rw-r--r-- | theories/Arith/Lt.v | 24 |
1 files changed, 12 insertions, 12 deletions
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. |