From 9ea33f07e98066cd05b5ab93f336f95e83272828 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 21 Jan 2021 04:54:34 +0900
Subject: Remove deprecation aliases introduced in 1.9.0

---
 CHANGELOG_UNRELEASED.md  |  5 +++++
 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.")]
-- 
cgit v1.2.3