remove deprecated commands whose deprecation was introduced in release 1.9.0

fixes #418

4 files changed, 14 insertions, 26 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9f859bb..7450661 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -125,6 +125,20 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Removed
 
+The following were deprecated since release 1.9.0
+- `tuple_perm_eqP` (use `tuple_permP` instead, from `perm.v`)
+- `eq_big_perm` (use `perm_big` instead, from `bigop.v`)
+- `perm_eqP` (use `permP` instead, from seq.v)
+- `perm_eqlP` (use `permPl` instead)
+- `perm_eqrP` (use `permPr` instead)
+- `perm_eqlE` (use `permEl` instead)
+- `perm_eq_refl` (use `perm_refl` instead)
+- `perm_eq_sym` (use `perm_sym` instead)
+- `perm_eq_trans` (use `perm_trans` instead)
+- `perm_eq_size` (use `perm_size` instead)
+- `perm_eq_mem` (use `perm_mem` instead)
+- `perm_eq_uniq` (use `perm_uniq` instead)
+
 ### Infrastructure
 
 ### Misc
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 34f230e..eb5e028 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -576,7 +576,3 @@ Qed.
 End LiftPerm.
 
 Prenex Implicits lift_perm lift_permK.
-
-Notation tuple_perm_eqP :=
-  (deprecate tuple_perm_eqP tuple_permP) (only parsing).
-
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 6d18825..633bb36 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1937,13 +1937,6 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
 Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed.
 Arguments biggcdn_inf [I] i0 [P F m].
 
-Notation "@ 'eq_big_perm'" :=
-  (deprecate eq_big_perm perm_big) (at level 10, only parsing).
-
-Notation eq_big_perm :=
-  ((fun R idx op I r1 P F r2 => @eq_big_perm R idx op I r1 r2 P F)
-        _   _  _ _  _ _ _) (only parsing).
-
 Notation filter_index_enum :=
   ((fun _ => @deprecated_filter_index_enum _)
      (deprecate filter_index_enum big_enumP)) (only parsing).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index f73c119..86a1545 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -3430,21 +3430,6 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
 Ltac tfae := do !apply: AllIffConj.
 
 (* Temporary backward compatibility. *)
-Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
-Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing).
-Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing).
-Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing).
-Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing).
-Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing).
-Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans)
-  (at level 10, only parsing).
-Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing).
-Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _)
-  (only parsing).
-Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _)
-  (only parsing).
-Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _)
-  (only parsing).
 Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
   (only parsing).
 Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)