2 files changed, 28 insertions, 20 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index dfcb5ac..9d01160 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -2732,6 +2732,7 @@ Arguments aut_groupAction {gT} G%g.
 Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
 Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.
 
-Notation pcycleE := (deprecate pcycleE porbitE _) (only parsing).
-Notation pcycle_actperm := (deprecate pcycle_actperm porbit_actperm _)
-  (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbitE instead.")]
+Notation pcycleE := porbitE (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit_actperm instead.")]
+Notation pcycle_actperm := porbit_actperm (only parsing).
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 5775e34..a54d2a6 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -693,20 +693,27 @@ Qed.
 
 End CastSn.
 
-Notation tuple_perm_eqP :=
-  (deprecate tuple_perm_eqP tuple_permP) (only parsing).
-Notation pcycle := (deprecate pcycle porbit _) (only parsing).
-Notation pcycles := (deprecate pcycles porbits _) (only parsing).
-Notation mem_pcycle := (deprecate mem_pcycle mem_porbit _) (only parsing).
-Notation pcycle_id := (deprecate pcycle_id porbit_id _) (only parsing).
-Notation uniq_traject_pcycle :=
-  (deprecate uniq_traject_pcycle uniq_traject_porbit _) (only parsing).
-Notation pcycle_traject := (deprecate pcycle_traject porbit_traject _)
-  (only parsing).
-Notation iter_pcycle := (deprecate iter_pcycle iter_porbit _) (only parsing).
-Notation eq_pcycle_mem := (deprecate eq_pcycle_mem eq_porbit_mem _)
-  (only parsing).
-Notation pcycle_sym := (deprecate pcycle_sym porbit_sym _) (only parsing).
-Notation pcycle_perm := (deprecate pcycle_perm porbit_perm _) (only parsing).
-Notation ncycles_mul_tperm := (deprecate ncycles_mul_tperm porbits_mul_tperm _)
-  (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use tuple_permP instead.")]
+Notation tuple_perm_eqP := tuple_permP (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit instead.")]
+Notation pcycle := porbit (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbits instead.")]
+Notation pcycles := porbits (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use mem_porbit instead.")]
+Notation mem_pcycle := mem_porbit (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit_id instead.")]
+Notation pcycle_id := porbit_id (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use uniq_traject_porbit instead.")]
+Notation uniq_traject_pcycle := uniq_traject_porbit (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit_traject instead.")]
+Notation pcycle_traject := porbit_traject (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use iter_porbit instead.")]
+Notation iter_pcycle := iter_porbit (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use eq_porbit_mem instead.")]
+Notation eq_pcycle_mem := eq_porbit_mem (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit_sym instead.")]
+Notation pcycle_sym := porbit_sym (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbit_perm instead.")]
+Notation pcycle_perm := porbit_perm (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use porbits_mul_tperm instead.")]
+Notation ncycles_mul_tperm := porbits_mul_tperm (only parsing).