diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 24 |
2 files changed, 5 insertions, 24 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fd5e2cb..c222c21 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -46,6 +46,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `ssrnat.v` and `ssrnum.v`, deprecation aliases and the `mc_1_10` compatibility modules introduced in MathComp 1.11+beta1 have been removed. +- in `seq.v`, remove the following deprecation aliases introduced in MathComp + 1.9.0: `perm_eq_rev`, `perm_eq_flatten`, `perm_eq_all`, `perm_eq_small`, + `perm_eq_nilP`, `perm_eq_consP`, `leq_size_perm`, `uniq_perm_eq`, + `perm_eq_iotaP`, and `perm_undup_count`. + ### Infrastructure ### Misc diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 401903a..e1e0ad4 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -4040,30 +4040,6 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := Ltac tfae := do !apply: AllIffConj. (* Temporary backward compatibility. *) -#[deprecated(since="mathcomp 1.9.0", note="Use perm_rev instead.")] -Notation perm_eq_rev := perm_rev (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_flatten instead.")] -Notation perm_eq_flatten := perm_flatten (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_all instead.")] -Notation perm_eq_all := perm_all (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_small_eq instead.")] -Notation perm_eq_small := perm_small_eq (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_nilP instead.")] -Notation perm_eq_nilP := perm_nilP (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_consP instead.")] -Notation perm_eq_consP := perm_consP (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use uniq_min_size instead.")] -Notation leq_size_perm := - ((fun T s1 s2 Us1 ss12 les21 => - let: (Esz12, Es12) := uniq_min_size T s1 s2 Us1 ss12 les21 - in conj Es12 Esz12) _ _ _) - (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use uniq_perm instead.")] -Notation uniq_perm_eq := uniq_perm (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_iotaP instead.")] -Notation perm_eq_iotaP := perm_iotaP (only parsing). -#[deprecated(since="mathcomp 1.9.0", note="Use perm_count_undup instead.")] -Notation perm_undup_count := perm_count_undup (only parsing). #[deprecated(since="mathcomp 1.11.0", note="Use takeD instead.")] Notation take_addn := takeD (only parsing). #[deprecated(since="mathcomp 1.11.0", note="Use rotD instead.")] |