Merge pull request #686 from pi8027/drop-coq-8.10

Drop support for Coq 8.10

24 files changed, 385 insertions, 1424 deletions

diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index b1603e6..2548614 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -31,7 +31,7 @@ TGTS?=
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
 COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
-COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq VDFILE=".coqdeps.test-suite" $(COQMAKEOPTIONS)
+COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS)
 BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
@@ -153,7 +153,6 @@ doc: __always__ Makefile.coq
 	. ../etc/utils/builddoc_lib.sh; \
 		cd _build_doc && mangle_sources $(COQFILES)
 	+cd _build_doc && $(COQMAKE)
-	cd _build_doc && if [ ! -f .Makefile.coq.d ] ; then cp .coqdeps.d .Makefile.coq.d ; fi #can be removed when coq-8.10 compatibility is dropped
 	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
 	cd _build_doc && cat depend | ../../etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
 	cd _build_doc && $(COQBIN)coqdoc -t "Mathematical Components" \
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 3efe76d..c99ef61 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -1075,11 +1075,11 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M.
 by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE.
 Qed.
 
-Notation "@ 'coprimez_expl'" :=
-  (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprimez_expr'" :=
-  (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope.
-Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing).
-Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing).
-Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing).
-Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMl instead.")]
+Notation coprimez_mull := coprimezMl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMr instead.")]
+Notation coprimez_mulr := coprimezMr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXl instead.")]
+Notation coprimez_expl := coprimezXl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXr instead.")]
+Notation coprimez_expr := coprimezXr (only parsing).
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index b6964f1..57d7c3c 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -876,444 +876,197 @@ Proof. exact: itv_splitUeq. Qed.
 
 End mc_1_11.
 
-(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a       *)
-(* qualified name.)                                                           *)
-Local Notation lteif := Order.lteif (only parsing).
-
+#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")]
 Notation "@ 'lersif'" :=
-  ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b))
-     (deprecate lersif lteif))
+  (fun (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b))
     (at level 10, only parsing).
 
-Notation lersif := (@lersif _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")]
+Notation lersif := (fun x y b => @Order.lteif _ _ x y (~~ b)) (only parsing).
 
+#[deprecated(since="mathcomp 1.12.0", note="Use [_ < _ ?<= if _] instead.")]
 Notation "x <= y ?< 'if' b" :=
-  ((fun _ => x < y ?<= if ~~ b) (deprecate lersif lteif))
-    (at level 70, y at next level, only parsing) : ring_scope.
+  (x < y ?<= if ~~ b) (at level 70, y at next level, only parsing) : ring_scope.
 
 (* LersifPo *)
 
-Notation "@ 'subr_lersifr0'" :=
-  ((fun _ => @mc_1_11.subr_lersifr0) (deprecate subr_lersifr0 subr_lteifr0))
-    (at level 10, only parsing).
-
-Notation subr_lersifr0 := (@subr_lersifr0 _) (only parsing).
-
-Notation "@ 'subr_lersif0r'" :=
-  ((fun _ => @mc_1_11.subr_lersif0r) (deprecate subr_lersif0r subr_lteif0r))
-    (at level 10, only parsing).
-
-Notation subr_lersif0r := (@subr_lersif0r _) (only parsing).
-
-Notation subr_lersif0 :=
-  ((fun _ => @mc_1_11.subr_lersif0) (deprecate subr_lersif0 subr_lteif0))
-    (only parsing).
-
-Notation "@ 'lersif_trans'" :=
-  ((fun _ => @mc_1_11.lersif_trans) (deprecate lersif_trans lteif_trans))
-    (at level 10, only parsing).
-
-Notation lersif_trans := (@lersif_trans _ _ _ _ _ _) (only parsing).
-
-Notation lersif01 :=
-  ((fun _ => @mc_1_11.lersif01) (deprecate lersif01 lteif01)) (only parsing).
-
-Notation "@ 'lersif_anti'" :=
-  ((fun _ => @mc_1_11.lersif_anti) (deprecate lersif_anti lteif_anti))
-    (at level 10, only parsing).
-
-Notation lersif_anti := (@lersif_anti _) (only parsing).
-
-Notation "@ 'lersifxx'" :=
-  ((fun _ => @mc_1_11.lersifxx) (deprecate lersifxx lteifxx))
-    (at level 10, only parsing).
-
-Notation lersifxx := (@lersifxx _) (only parsing).
-
-Notation "@ 'lersifNF'" :=
-  ((fun _ => @mc_1_11.lersifNF) (deprecate lersifNF lteifNF))
-    (at level 10, only parsing).
-
-Notation lersifNF := (@lersifNF _ _ _ _) (only parsing).
-
-Notation "@ 'lersifS'" :=
-  ((fun _ => @mc_1_11.lersifS) (deprecate lersifS lteifS))
-    (at level 10, only parsing).
-
-Notation lersifS := (@lersifS _ _ _) (only parsing).
-
-Notation "@ 'lersifT'" :=
-  ((fun _ => @mc_1_11.lersifT) (deprecate lersifT lteifT))
-    (at level 10, only parsing).
-
-Notation lersifT := (@lersifT _) (only parsing).
-
-Notation "@ 'lersifF'" :=
-  ((fun _ => @mc_1_11.lersifF) (deprecate lersifF lteifF))
-    (at level 10, only parsing).
-
-Notation lersifF := (@lersifF _) (only parsing).
-
-Notation "@ 'lersif_oppl'" :=
-  ((fun _ => @mc_1_11.lersif_oppl) (deprecate lersif_oppl lteif_oppl))
-    (at level 10, only parsing).
-
-Notation lersif_oppl := (@lersif_oppl _) (only parsing).
-
-Notation "@ 'lersif_oppr'" :=
-  ((fun _ => @mc_1_11.lersif_oppr) (deprecate lersif_oppr lteif_oppr))
-    (at level 10, only parsing).
-
-Notation lersif_oppr := (@lersif_oppr _) (only parsing).
-
-Notation "@ 'lersif_0oppr'" :=
-  ((fun _ => @mc_1_11.lersif_0oppr) (deprecate lersif_0oppr lteif_0oppr))
-    (at level 10, only parsing).
-
-Notation lersif_0oppr := (@lersif_0oppr _) (only parsing).
-
-Notation "@ 'lersif_oppr0'" :=
-  ((fun _ => @mc_1_11.lersif_oppr0) (deprecate lersif_oppr0 lteif_oppr0))
-    (at level 10, only parsing).
-
-Notation lersif_oppr0 := (@lersif_oppr0 _) (only parsing).
-
-Notation "@ 'lersif_opp2'" :=
-  ((fun _ => @mc_1_11.lersif_opp2) (deprecate lersif_opp2 lteif_opp2))
-    (at level 10, only parsing).
-
-Notation lersif_opp2 := (@lersif_opp2 _) (only parsing).
-
-Notation lersif_oppE :=
-  ((fun _ => @mc_1_11.lersif_oppE) (deprecate lersif_oppE lteif_oppE))
-    (only parsing).
-
-Notation "@ 'lersif_add2l'" :=
-  ((fun _ => @mc_1_11.lersif_add2l) (deprecate lersif_add2l lteif_add2l))
-    (at level 10, only parsing).
-
-Notation lersif_add2l := (@lersif_add2l _) (only parsing).
-
-Notation "@ 'lersif_add2r'" :=
-  ((fun _ => @mc_1_11.lersif_add2r) (deprecate lersif_add2r lteif_add2r))
-    (at level 10, only parsing).
-
-Notation lersif_add2r := (@lersif_add2r _) (only parsing).
-
-Notation lersif_add2 :=
-  ((fun _ => @mc_1_11.lersif_add2) (deprecate lersif_add2 lteif_add2))
-    (only parsing).
-
-Notation "@ 'lersif_subl_addr'" :=
-  ((fun _ => @mc_1_11.lersif_subl_addr)
-     (deprecate lersif_subl_addr lteif_subl_addr))
-    (at level 10, only parsing).
-
-Notation lersif_subl_addr := (@lersif_subl_addr _) (only parsing).
-
-Notation "@ 'lersif_subr_addr'" :=
-  ((fun _ => @mc_1_11.lersif_subr_addr)
-     (deprecate lersif_subr_addr lteif_subr_addr))
-    (at level 10, only parsing).
-
-Notation lersif_subr_addr := (@lersif_subr_addr _) (only parsing).
-
-Notation lersif_sub_addr :=
-  ((fun _ => @mc_1_11.lersif_sub_addr)
-     (deprecate lersif_sub_addr lteif_sub_addr))
-    (only parsing).
-
-Notation "@ 'lersif_subl_addl'" :=
-  ((fun _ => @mc_1_11.lersif_subl_addl)
-     (deprecate lersif_subl_addl lteif_subl_addl))
-    (at level 10, only parsing).
-
-Notation lersif_subl_addl := (@lersif_subl_addl _) (only parsing).
-
-Notation "@ 'lersif_subr_addl'" :=
-  ((fun _ => @mc_1_11.lersif_subr_addl)
-     (deprecate lersif_subr_addl lteif_subr_addl))
-    (at level 10, only parsing).
-
-Notation lersif_subr_addl := (@lersif_subr_addl _) (only parsing).
-
-Notation lersif_sub_addl :=
-  ((fun _ => @mc_1_11.lersif_sub_addl)
-     (deprecate lersif_sub_addl lteif_sub_addl))
-    (only parsing).
-
-Notation "@ 'lersif_andb'" :=
-  ((fun _ => @mc_1_11.lersif_andb) (deprecate lersif_andb lteif_andb))
-    (at level 10, only parsing).
-
-Notation lersif_andb := (@lersif_andb _) (only parsing).
-
-Notation "@ 'lersif_orb'" :=
-  ((fun _ => @mc_1_11.lersif_orb) (deprecate lersif_orb lteif_orb))
-    (at level 10, only parsing).
-
-Notation lersif_orb := (@lersif_orb _) (only parsing).
-
-Notation "@ 'lersif_imply'" :=
-  ((fun _ => @mc_1_11.lersif_imply) (deprecate lersif_imply lteif_imply))
-    (at level 10, only parsing).
-
-Notation lersif_imply := (@lersif_imply _ _ _ _ _) (only parsing).
-
-Notation "@ 'lersifW'" :=
-  ((fun _ => @mc_1_11.lersifW) (deprecate lersifW lteifW))
-    (at level 10, only parsing).
-
-Notation lersifW := (@lersifW _ _ _ _) (only parsing).
-
-Notation "@ 'ltrW_lersif'" :=
-  ((fun _ => @mc_1_11.ltrW_lersif) (deprecate ltrW_lersif ltrW_lteif))
-    (at level 10, only parsing).
-
-Notation ltrW_lersif := (@ltrW_lersif _) (only parsing).
-
-Notation "@ 'lersif_pmul2l'" :=
-  ((fun _ => @mc_1_11.lersif_pmul2l) (deprecate lersif_pmul2l lteif_pmul2l))
-    (at level 10, only parsing).
-
-Notation lersif_pmul2l := (fun b => @lersif_pmul2l _ b _) (only parsing).
-
-Notation "@ 'lersif_pmul2r'" :=
-  ((fun _ => @mc_1_11.lersif_pmul2r) (deprecate lersif_pmul2r lteif_pmul2r))
-    (at level 10, only parsing).
-
-Notation lersif_pmul2r := (fun b => @lersif_pmul2r _ b _) (only parsing).
-
-Notation "@ 'lersif_nmul2l'" :=
-  ((fun _ => @mc_1_11.lersif_nmul2l) (deprecate lersif_nmul2l lteif_nmul2l))
-    (at level 10, only parsing).
-
-Notation lersif_nmul2l := (fun b => @lersif_nmul2l _ b _) (only parsing).
-
-Notation "@ 'lersif_nmul2r'" :=
-  ((fun _ => @mc_1_11.lersif_nmul2r) (deprecate lersif_nmul2r lteif_nmul2r))
-    (at level 10, only parsing).
-
-Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing).
-
-Notation "@ 'real_lersifN'" :=
-  ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE))
-    (at level 10, only parsing).
-
-Notation real_lersifN := (@real_lersifN _ _ _) (only parsing).
-
-Notation "@ 'real_lersif_norml'" :=
-  ((fun _ => @mc_1_11.real_lersif_norml)
-     (deprecate real_lersif_norml real_lteif_norml))
-    (at level 10, only parsing).
-
-Notation real_lersif_norml :=
-  (fun b => @real_lersif_norml _ b _) (only parsing).
-
-Notation "@ 'real_lersif_normr'" :=
-  ((fun _ => @mc_1_11.real_lersif_normr)
-     (deprecate real_lersif_normr real_lteif_normr))
-    (at level 10, only parsing).
-
-Notation real_lersif_normr :=
-  (fun b x => @real_lersif_normr _ b x _) (only parsing).
-
-Notation "@ 'lersif_nnormr'" :=
-  ((fun _ => @mc_1_11.lersif_nnormr) (deprecate lersif_nnormr lteif_nnormr))
-    (at level 10, only parsing).
-
-Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteifr0 instead.")]
+Notation subr_lersifr0 := mc_1_11.subr_lersifr0 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0r instead.")]
+Notation subr_lersif0r := mc_1_11.subr_lersif0r (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0 instead.")]
+Notation subr_lersif0 := mc_1_11.subr_lersif0 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_trans instead.")]
+Notation lersif_trans := mc_1_11.lersif_trans (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif01 instead.")]
+Notation lersif01 := mc_1_11.lersif01 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_anti instead.")]
+Notation lersif_anti := mc_1_11.lersif_anti (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifxx instead.")]
+Notation lersifxx := mc_1_11.lersifxx (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifNF instead.")]
+Notation lersifNF := mc_1_11.lersifNF (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifS instead.")]
+Notation lersifS := mc_1_11.lersifS (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifT instead.")]
+Notation lersifT := mc_1_11.lersifT (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifF instead.")]
+Notation lersifF := mc_1_11.lersifF (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppl instead.")]
+Notation lersif_oppl := mc_1_11.lersif_oppl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr instead.")]
+Notation lersif_oppr := mc_1_11.lersif_oppr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_0oppr instead.")]
+Notation lersif_0oppr := mc_1_11.lersif_0oppr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr0 instead.")]
+Notation lersif_oppr0 := mc_1_11.lersif_oppr0 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_opp2 instead.")]
+Notation lersif_opp2 := mc_1_11.lersif_opp2 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppE instead.")]
+Notation lersif_oppE := mc_1_11.lersif_oppE (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2l instead.")]
+Notation lersif_add2l := mc_1_11.lersif_add2l (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2r instead.")]
+Notation lersif_add2r := mc_1_11.lersif_add2r (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2 instead.")]
+Notation lersif_add2 := mc_1_11.lersif_add2 (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subl_addr instead.")]
+Notation lersif_subl_addr := mc_1_11.lersif_subl_addr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subr_addr instead.")]
+Notation lersif_subr_addr := mc_1_11.lersif_subr_addr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_sub_addr instead.")]
+Notation lersif_sub_addr := mc_1_11.lersif_sub_addr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subl_addl instead.")]
+Notation lersif_subl_addl := mc_1_11.lersif_subl_addl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subr_addl instead.")]
+Notation lersif_subr_addl := mc_1_11.lersif_subr_addl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lersif_sub_addl instead.")]
+Notation lersif_sub_addl := mc_1_11.lersif_sub_addl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_andb instead.")]
+Notation lersif_andb := mc_1_11.lersif_andb (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_orb instead.")]
+Notation lersif_orb := mc_1_11.lersif_orb (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_imply instead.")]
+Notation lersif_imply := mc_1_11.lersif_imply (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifW instead.")]
+Notation lersifW := mc_1_11.lersifW (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use ltrW_lteif instead.")]
+Notation ltrW_lersif := mc_1_11.ltrW_lersif (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2l instead.")]
+Notation lersif_pmul2l := mc_1_11.lersif_pmul2l (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2r instead.")]
+Notation lersif_pmul2r := mc_1_11.lersif_pmul2r (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2l instead.")]
+Notation lersif_nmul2l := mc_1_11.lersif_nmul2l (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2r instead.")]
+Notation lersif_nmul2r := mc_1_11.lersif_nmul2r (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use real_lteifNE instead.")]
+Notation real_lersifN := mc_1_11.real_lersifN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_norml instead.")]
+Notation real_lersif_norml := mc_1_11.real_lersif_norml (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_normr instead.")]
+Notation real_lersif_normr := mc_1_11.real_lersif_normr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nnormr instead.")]
+Notation lersif_nnormr := mc_1_11.lersif_nnormr (only parsing).
 
 (* LersifOrdered *)
 
-Notation "@ 'lersifN'" :=
-  ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE))
-    (at level 10, only parsing).
-
-Notation lersifN := (@lersifN _) (only parsing).
-
-Notation "@ 'lersif_norml'" :=
-  ((fun _ => @mc_1_11.lersif_norml) (deprecate lersif_norml lteif_norml))
-    (at level 10, only parsing).
-
-Notation lersif_norml := (@lersif_norml _) (only parsing).
-
-Notation "@ 'lersif_normr'" :=
-  ((fun _ => @mc_1_11.lersif_normr) (deprecate lersif_normr lteif_normr))
-    (at level 10, only parsing).
-
-Notation lersif_normr := (@lersif_normr _) (only parsing).
-
-Notation "@ 'lersif_distl'" :=
-  ((fun _ => @mc_1_11.lersif_distl) (deprecate lersif_distl lteif_distl))
-    (at level 10, only parsing).
-
-Notation lersif_distl := (@lersif_distl _) (only parsing).
-
-Notation "@ 'lersif_minr'" :=
-  ((fun _ => @mc_1_11.lersif_minr) (deprecate lersif_minr lteif_minr))
-    (at level 10, only parsing).
-
-Notation lersif_minr := (@lersif_minr _) (only parsing).
-
-Notation "@ 'lersif_minl'" :=
-  ((fun _ => @mc_1_11.lersif_minl) (deprecate lersif_minl lteif_minl))
-    (at level 10, only parsing).
-
-Notation lersif_minl := (@lersif_minl _) (only parsing).
-
-Notation "@ 'lersif_maxr'" :=
-  ((fun _ => @mc_1_11.lersif_maxr) (deprecate lersif_maxr lteif_maxr))
-    (at level 10, only parsing).
-
-Notation lersif_maxr := (@lersif_maxr _) (only parsing).
-
-Notation "@ 'lersif_maxl'" :=
-  ((fun _ => @mc_1_11.lersif_maxl) (deprecate lersif_maxl lteif_maxl))
-    (at level 10, only parsing).
-
-Notation lersif_maxl := (@lersif_maxl _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteifNE instead.")]
+Notation lersifN := mc_1_11.lersifN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_norml instead.")]
+Notation lersif_norml := mc_1_11.lersif_norml (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_normr instead.")]
+Notation lersif_normr := mc_1_11.lersif_normr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_distl instead.")]
+Notation lersif_distl := mc_1_11.lersif_distl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minr instead.")]
+Notation lersif_minr := mc_1_11.lersif_minr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minl instead.")]
+Notation lersif_minl := mc_1_11.lersif_minl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxr instead.")]
+Notation lersif_maxr := mc_1_11.lersif_maxr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxl instead.")]
+Notation lersif_maxl := mc_1_11.lersif_maxl (only parsing).
 
 (* LersifField *)
 
-Notation "@ 'lersif_pdivl_mulr'" :=
-  ((fun _ => @mc_1_11.lersif_pdivl_mulr)
-     (deprecate lersif_pdivl_mulr lteif_pdivl_mulr))
-    (at level 10, only parsing).
-
-Notation lersif_pdivl_mulr :=
-  (fun b => @lersif_pdivl_mulr _ b _) (only parsing).
-
-Notation "@ 'lersif_pdivr_mulr'" :=
-  ((fun _ => @mc_1_11.lersif_pdivr_mulr)
-     (deprecate lersif_pdivr_mulr lteif_pdivr_mulr))
-    (at level 10, only parsing).
-
-Notation lersif_pdivr_mulr :=
-  (fun b => @lersif_pdivr_mulr _ b _) (only parsing).
-
-Notation "@ 'lersif_pdivl_mull'" :=
-  ((fun _ => @mc_1_11.lersif_pdivl_mull)
-     (deprecate lersif_pdivl_mull lteif_pdivl_mull))
-    (at level 10, only parsing).
-
-Notation lersif_pdivl_mull :=
-  (fun b => @lersif_pdivl_mull _ b _) (only parsing).
-
-Notation "@ 'lersif_pdivr_mull'" :=
-  ((fun _ => @mc_1_11.lersif_pdivr_mull)
-     (deprecate lersif_pdivr_mull lteif_pdivr_mull))
-    (at level 10, only parsing).
-
-Notation lersif_pdivr_mull :=
-  (fun b => @lersif_pdivr_mull _ b _) (only parsing).
-
-Notation "@ 'lersif_ndivl_mulr'" :=
-  ((fun _ => @mc_1_11.lersif_ndivl_mulr)
-     (deprecate lersif_ndivl_mulr lteif_ndivl_mulr))
-    (at level 10, only parsing).
-
-Notation lersif_ndivl_mulr :=
-  (fun b => @lersif_ndivl_mulr _ b _) (only parsing).
-
-Notation "@ 'lersif_ndivr_mulr'" :=
-  ((fun _ => @mc_1_11.lersif_ndivr_mulr)
-     (deprecate lersif_ndivr_mulr lteif_ndivr_mulr))
-    (at level 10, only parsing).
-
-Notation lersif_ndivr_mulr :=
-  (fun b => @lersif_ndivr_mulr _ b _) (only parsing).
-
-Notation "@ 'lersif_ndivl_mull'" :=
-  ((fun _ => @mc_1_11.lersif_ndivl_mull)
-     (deprecate lersif_ndivl_mull lteif_ndivl_mull))
-    (at level 10, only parsing).
-
-Notation lersif_ndivl_mull :=
-  (fun b => @lersif_ndivl_mull _ b _) (only parsing).
-
-Notation "@ 'lersif_ndivr_mull'" :=
-  ((fun _ => @mc_1_11.lersif_ndivr_mull)
-     (deprecate lersif_ndivr_mull lteif_ndivr_mull))
-    (at level 10, only parsing).
-
-Notation lersif_ndivr_mull :=
-  (fun b => @lersif_ndivr_mull _ b _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mulr instead.")]
+Notation lersif_pdivl_mulr := mc_1_11.lersif_pdivl_mulr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mulr instead.")]
+Notation lersif_pdivr_mulr := mc_1_11.lersif_pdivr_mulr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mull instead.")]
+Notation lersif_pdivl_mull := mc_1_11.lersif_pdivl_mull (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mull instead.")]
+Notation lersif_pdivr_mull := mc_1_11.lersif_pdivr_mull (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mulr instead.")]
+Notation lersif_ndivl_mulr := mc_1_11.lersif_ndivl_mulr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mulr instead.")]
+Notation lersif_ndivr_mulr := mc_1_11.lersif_ndivr_mulr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mull instead.")]
+Notation lersif_ndivl_mull := mc_1_11.lersif_ndivl_mull (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mull instead.")]
+Notation lersif_ndivr_mull := mc_1_11.lersif_ndivr_mull (only parsing).
 
 (* IntervalPo *)
 
-Notation "@ 'lersif_in_itv'" :=
-  ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv))
-    (at level 10, only parsing).
-
-Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing).
-
-Notation "@ 'itv_gte'" :=
-  ((fun _ => @mc_1_11.itv_gte) (deprecate itv_gte itv_ge))
-    (at level 10, only parsing).
-
-Notation itv_gte := (@itv_gte _ _ _ _ _) (only parsing).
-
-Notation "@ 'ltr_in_itv'" :=
-  ((fun _ => @mc_1_11.ltr_in_itv) (deprecate ltr_in_itv lt_in_itv))
-    (at level 10, only parsing).
-
-Notation ltr_in_itv := (@ltr_in_itv _ _ _ _ _ _) (only parsing).
-
-Notation "@ 'ler_in_itv'" :=
-  ((fun _ => @mc_1_11.ler_in_itv) (deprecate ler_in_itv lt_in_itv))
-    (at level 10, only parsing).
-
-Notation ler_in_itv := (@ler_in_itv _ _ _ _ _ _) (only parsing).
-
-Notation "@ 'itv_splitU2'" :=
-  ((fun _ => @mc_1_11.itv_splitU2) (deprecate itv_splitU2 itv_splitUeq))
-    (at level 10, only parsing).
-
-Notation itv_splitU2 := (@itv_splitU2 _ _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lteif_in_itv instead.")]
+Notation lersif_in_itv := mc_1_11.lersif_in_itv (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use itv_ge instead.")]
+Notation itv_gte := mc_1_11.itv_gte (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")]
+Notation ltr_in_itv := mc_1_11.ltr_in_itv (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")]
+Notation ler_in_itv := @mc_1_11.ler_in_itv (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use itv_splitUeq instead.")]
+Notation itv_splitU2 := mc_1_11.itv_splitU2 (only parsing).
 
 (* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts    *)
-(* only `realDomainType`. Use `Order.meet` instead of `itv_meet`.             *)
+(* only `realDomainType`.                                                     *)
+#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")]
 Notation "@ 'itv_intersection'" :=
-  ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R])
-     (deprecate itv_intersection itv_meet))
+  (fun (R : realDomainType) => @Order.meet _ [latticeType of interval R])
     (at level 10, only parsing) : fun_scope.
+#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")]
+Notation itv_intersection :=
+  (@Order.meet _ [latticeType of interval (_ : realDomainType)]) (only parsing).
 
-Notation itv_intersection := (@itv_intersection _) (only parsing).
-
+#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")]
 Notation "@ 'itv_intersection1i'" :=
-  ((fun _ (R : realDomainType) => @meet1x _ [tbLatticeType of interval R])
-     (deprecate itv_intersection1i meet1x))
+  (fun (R : realDomainType) => @meet1x _ [tbLatticeType of interval R])
     (at level 10, only parsing) : fun_scope.
+#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")]
+Notation itv_intersection1i :=
+  (@meet1x _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing).
 
-Notation itv_intersection1i := (@itv_intersection1i _) (only parsing).
-
+#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")]
 Notation "@ 'itv_intersectioni1'" :=
-  ((fun _ (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R])
-     (deprecate itv_intersectioni1 meetx1))
+  (fun (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R])
     (at level 10, only parsing) : fun_scope.
+#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")]
+ Notation itv_intersectioni1 :=
+  (@meetx1 _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing).
 
-Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing).
-
+#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")]
 Notation "@ 'itv_intersectionii'" :=
-  ((fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R])
-     (deprecate itv_intersectionii meetxx))
+  (fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R])
     (at level 10, only parsing) : fun_scope.
-
-Notation itv_intersectionii := (@itv_intersectionii _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")]
+Notation itv_intersectionii :=
+  (@meetxx _ [latticeType of interval (_ : realDomainType)]) (only parsing).
 
 (* IntervalOrdered *)
-
+#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")]
 Notation "@ 'itv_intersectionC'" :=
-  ((fun _ (R : realDomainType) => @meetC _ [latticeType of interval R])
-     (deprecate itv_intersectionC meetC))
+  (fun (R : realDomainType) => @meetC _ [latticeType of interval R])
     (at level 10, only parsing) : fun_scope.
+#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")]
+Notation itv_intersectionC :=
+  (@meetC _ [latticeType of interval (_ : realDomainType)]) (only parsing).
 
-Notation itv_intersectionC := (@itv_intersectionC _) (only parsing).
-
+#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")]
 Notation "@ 'itv_intersectionA'" :=
-  ((fun _ (R : realDomainType) => @meetA _ [latticeType of interval R])
-     (deprecate itv_intersectionA meetA))
+  (fun (R : realDomainType) => @meetA _ [latticeType of interval R])
     (at level 10, only parsing) : fun_scope.
-
-Notation itv_intersectionA := (@itv_intersectionA _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")]
+Notation itv_intersectionA :=
+  (@meetA _ [latticeType of interval (_ : realDomainType)]) (only parsing).
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index e7e0e35..bd39654 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -3146,9 +3146,8 @@ Canonical matrix_finAlgType (R : finComRingType) n' :=
 
 Hint Resolve comm_mx_scalar comm_scalar_mx : core.
 
-Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar)
-  (at level 10, only parsing) : fun_scope.
-Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use comm_mx_scalar instead.")]
+Notation scalar_mx_comm := comm_mx_scalar (only parsing).
 
 (*****************************************************************************)
 (********************** Matrix unit ring and inverse matrices ****************)
@@ -3685,6 +3684,5 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S)
 End mxRingOver.
 End mxOver.
 
-Notation "@ 'map_mx_sub'" :=
-  (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope.
-Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use map_mxB instead.")]
+Notation map_mx_sub := map_mxB (only parsing).
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index d707905..c23cfb1 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -3068,9 +3068,7 @@ Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed.
 
 End MapMatrixSpaces.
 
-Notation "@ 'mulsmx_addl'" :=
-  (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'mulsmx_addr'" :=
-  (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope.
-Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing).
-Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDl instead.")]
+Notation mulsmx_addl := mulsmxDl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDr instead.")]
+Notation mulsmx_addr := mulsmxDr (only parsing).
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 21e8ada..e74c917 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -2769,27 +2769,19 @@ Qed.
 
 End ClosedField.
 
-Notation "@ 'polyC_add'" :=
-  (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_opp'" :=
-  (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_sub'" :=
-  (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_muln'" :=
-  (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_mul'" :=
-  (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope.
-Notation "@ 'polyC_inv'" :=
-  (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope.
-Notation "@ 'lead_coef_opp'" :=
-  (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'derivn_sub'" :=
-  (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope.
-Notation polyC_add := (@polyC_add _) (only parsing).
-Notation polyC_opp := (@polyC_opp _) (only parsing).
-Notation polyC_sub := (@polyC_sub _) (only parsing).
-Notation polyC_muln := (@polyC_muln _) (only parsing).
-Notation polyC_mul := (@polyC_mul _) (only parsing).
-Notation polyC_inv := (@polyC_inv _) (only parsing).
-Notation lead_coef_opp := (@lead_coef_opp _) (only parsing).
-Notation derivn_sub := (@derivn_sub _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCD instead.")]
+Notation polyC_add := polyCD (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCN instead.")]
+Notation polyC_opp := polyCN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCB instead.")]
+Notation polyC_sub := polyCB (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCMn instead.")]
+Notation polyC_muln := polyCMn (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCM instead.")]
+Notation polyC_mul := polyCM (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCV instead.")]
+Notation polyC_inv := polyCV (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lead_coefN instead.")]
+Notation lead_coef_opp := lead_coefN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use derivnB instead.")]
+Notation derivn_sub := derivnB (only parsing).
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 41147fb..05a9ee3 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -624,17 +624,12 @@ Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed.
 
 End MonicDivisor.
 
-Notation "@ 'rdivp_addl'" :=
-  (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'rdivp_addr'" :=
-  (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'rmodp_add'" :=
-  (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope.
-Notation rdivp_addl :=
-  (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing).
-Notation rdivp_addr :=
-  (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing).
-Notation rmodp_add := (@rmodp_add _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDl instead.")]
+Notation rdivp_addl := rdivpDl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDr instead.")]
+Notation rdivp_addr := rdivpDr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use rmodpD instead.")]
+Notation rmodp_add := rmodpD (only parsing).
 
 End RingMonic.
 
@@ -2358,27 +2353,20 @@ End IDomainPseudoDivision.
 Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core.
 Hint Resolve dvdp0 : core.
 
-Notation "@ 'dvdp_scalel'" :=
-  (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'dvdp_scaler'" :=
-  (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'dvdp_opp'" :=
-  (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprimep_scalel'" :=
-  (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprimep_scaler'" :=
-  (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprimep_mull'" :=
-  (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprimep_mulr'" :=
-  (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope.
-Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing).
-Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing).
-Notation dvdp_opp := (@dvdp_opp _) (only parsing).
-Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing).
-Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing).
-Notation coprimep_mull := (@coprimep_mull _) (only parsing).
-Notation coprimep_mulr := (@coprimep_mulr _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZl instead.")]
+Notation dvdp_scalel := dvdpZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZr instead.")]
+Notation dvdp_scaler := dvdpZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use dvdpNr instead.")]
+Notation dvdp_opp := dvdpNr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZl instead.")]
+Notation coprimep_scalel := coprimepZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZr instead.")]
+Notation coprimep_scaler := coprimepZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMl instead.")]
+Notation coprimep_mull := coprimepMl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMr instead.")]
+Notation coprimep_mulr := coprimepMr (only parsing).
 
 End CommonIdomain.
 
@@ -2704,30 +2692,22 @@ Qed.
 
 End MoreUnitDivisor.
 
-Notation "@ 'modp_scalel'" :=
-  (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_scaler'" :=
-  (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_opp'" :=
-  (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_add'" :=
-  (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_scalel'" :=
-  (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_scaler'" :=
-  (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_opp'" :=
-  (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_add'" :=
-  (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope.
-Notation modp_scalel := (@modp_scalel _ _) (only parsing).
-Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing).
-Notation modp_opp := (@modp_opp _ _) (only parsing).
-Notation modp_add := (@modp_add _ _) (only parsing).
-Notation divp_scalel := (@divp_scalel _ _) (only parsing).
-Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing).
-Notation divp_opp := (@divp_opp _ _) (only parsing).
-Notation divp_add := (@divp_add _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")]
+Notation modp_scalel := modpZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")]
+Notation modp_scaler := modpZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")]
+Notation modp_opp := modpN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")]
+Notation modp_add := modpD (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")]
+Notation divp_scalel := divpZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")]
+Notation divp_scaler := divpZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")]
+Notation divp_opp := divpN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")]
+Notation divp_add := divpD (only parsing).
 
 End IdomainUnit.
 
@@ -3192,30 +3172,22 @@ End FieldMap.
 
 End FieldDivision.
 
-Notation "@ 'modp_scalel'" :=
-  (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_scaler'" :=
-  (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_opp'" :=
-  (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'modp_add'" :=
-  (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_scalel'" :=
-  (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_scaler'" :=
-  (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_opp'" :=
-  (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'divp_add'" :=
-  (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope.
-Notation modp_scalel := (@modp_scalel _) (only parsing).
-Notation modp_scaler := (@modp_scaler _ _) (only parsing).
-Notation modp_opp := (@modp_opp _) (only parsing).
-Notation modp_add := (@modp_add _) (only parsing).
-Notation divp_scalel := (@divp_scalel _) (only parsing).
-Notation divp_scaler := (@divp_scaler _ _) (only parsing).
-Notation divp_opp := (@divp_opp _) (only parsing).
-Notation divp_add := (@divp_add _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")]
+Notation modp_scalel := modpZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")]
+Notation modp_scaler := modpZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")]
+Notation modp_opp := modpN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")]
+Notation modp_add := modpD (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")]
+Notation divp_scalel := divpZl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")]
+Notation divp_scaler := divpZr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")]
+Notation divp_opp := divpN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")]
+Notation divp_add := divpD (only parsing).
 
 End Field.
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index de8b513..a27177d 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -6044,8 +6044,8 @@ Definition imaginary_exists := imaginary_exists.
 Notation null_fun V := (null_fun V) (only parsing).
 Notation in_alg A := (in_alg_loc A).
 
-Notation prodrMn :=
- (fun n A F => deprecate prodrMn prodrMn_const _ n _ A F) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use prodrMn_const instead.")]
+Notation prodrMn := prodrMn_const (only parsing).
 
 End Theory.
 
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index a51ec47..becacc2 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1778,6 +1778,5 @@ Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed.
 
 End rpred.
 
-Notation "@ 'polyC_mulrz'" :=
-  (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope.
-Notation polyC_mulrz := (@polyC_mulrz _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")]
+Notation polyC_mulrz := polyCMz (only parsing).
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index dce3ffd..cc04183 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -5395,625 +5395,3 @@ Export Num.NumMixin.Exports Num.RealMixin.Exports.
 Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports.
 
 Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.
-
-(* compatibility module *)
-Module mc_1_10.
-Module Num.
-(* If you failed to process the next line in the PG or the CoqIDE, replace    *)
-(* all the "ssrnum.Num" with "Top.Num" in this module to process them, and    *)
-(* revert them in order to compile and commit.  This problem will be solved   *)
-(* in Coq 8.10.  See also: https://github.com/math-comp/math-comp/pull/270.   *)
-Export ssrnum.Num.
-
-Module Import Def.
-Export ssrnum.Num.Def.
-Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y.
-Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x.
-End Def.
-
-Notation min := minr.
-Notation max := maxr.
-
-Module Import Syntax.
-Notation "`| x |" :=
-  (@norm _ (@Num.NormedZmodule.numDomain_normedZmodType _) x) : ring_scope.
-End Syntax.
-
-Module Import Theory.
-Export ssrnum.Num.Theory.
-
-Section NumIntegralDomainTheory.
-Variable R : numDomainType.
-Implicit Types x y z : R.
-Definition ltr_def x y : (x < y) = (y != x) && (x <= y) := lt_def x y.
-Definition gerE x y : ge x y = (y <= x) := geE x y.
-Definition gtrE x y : gt x y = (y < x) := gtE x y.
-Definition lerr x : x <= x := lexx x.
-Definition ltrr x : x < x = false := ltxx x.
-Definition ltrW x y : x < y -> x <= y := @ltW _ _ x y.
-Definition ltr_neqAle x y : (x < y) = (x != y) && (x <= y) := lt_neqAle x y.
-Definition ler_eqVlt x y : (x <= y) = (x == y) || (x < y) := le_eqVlt x y.
-Definition gtr_eqF x y : y < x -> x == y = false := @gt_eqF _ _ x y.
-Definition ltr_eqF x y : x < y -> x == y = false := @lt_eqF _ _ x y.
-Definition ler_asym : antisymmetric (@ler R) := le_anti.
-Definition eqr_le x y : (x == y) = (x <= y <= x) := eq_le x y.
-Definition ltr_trans : transitive (@ltr R) := lt_trans.
-Definition ler_lt_trans y x z : x <= y -> y < z -> x < z :=
-  @le_lt_trans _ _ y x z.
-Definition ltr_le_trans y x z : x < y -> y <= z -> x < z :=
-  @lt_le_trans _ _ y x z.
-Definition ler_trans : transitive (@ler R) := le_trans.
-Definition lterr := (lerr, ltrr).
-Definition lerifP x y C :
-  reflect (x <= y ?= iff C) (if C then x == y else x < y) := leifP.
-Definition ltr_asym x y : x < y < x = false := lt_asym x y.
-Definition ler_anti : antisymmetric (@ler R) := le_anti.
-Definition ltr_le_asym x y : x < y <= x = false := lt_le_asym x y.
-Definition ler_lt_asym x y : x <= y < x = false := le_lt_asym x y.
-Definition lter_anti := (=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym).
-Definition ltr_geF x y : x < y -> y <= x = false := @lt_geF _ _ x y.
-Definition ler_gtF x y : x <= y -> y < x = false := @le_gtF _ _ x y.
-Definition ltr_gtF x y : x < y -> y < x = false := @lt_gtF _ _ x y.
-Definition normr0 : `|0| = 0 :> R := normr0 _.
-Definition normrMn x n : `|x *+ n| = `|x| *+ n := normrMn x n.
-Definition normr0P {x} : reflect (`|x| = 0) (x == 0) := normr0P.
-Definition normr_eq0 x : (`|x| == 0) = (x == 0) := normr_eq0 x.
-Definition normrN x : `|- x| = `|x| := normrN x.
-Definition distrC x y : `|x - y| = `|y - x| := distrC x y.
-Definition normr_id x : `| `|x| | = `|x| := normr_id x.
-Definition normr_ge0 x : 0 <= `|x| := normr_ge0 x.
-Definition normr_le0 x : (`|x| <= 0) = (x == 0) := normr_le0 x.
-Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x.
-Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x.
-Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0,
-                      normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN).
-End NumIntegralDomainTheory.
-
-Section NumIntegralDomainMonotonyTheory.
-Variables R R' : numDomainType.
-Section AcrossTypes.
-Variables (D D' : pred R) (f : R -> R').
-Definition ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y} :=
-  ltW_homo (f := f).
-Definition ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y} :=
-  ltW_nhomo (f := f).
-Definition inj_homo_ltr :
-  injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y} :=
-  inj_homo_lt (f := f).
-Definition inj_nhomo_ltr :
-  injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y} :=
-  inj_nhomo_lt (f := f).
-Definition incr_inj : {mono f : x y / x <= y} -> injective f :=
-  inc_inj (f := f).
-Definition decr_inj : {mono f : x y /~ x <= y} -> injective f :=
-  dec_inj (f := f).
-Definition lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y} :=
-  leW_mono (f := f).
-Definition lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y} :=
-  leW_nmono (f := f).
-Definition ltrW_homo_in :
-  {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}} :=
-  ltW_homo_in (f := f).
-Definition ltrW_nhomo_in :
-  {in D & D', {homo f : x y /~ x < y}} ->
-  {in D & D', {homo f : x y /~ x <= y}} :=
-  ltW_nhomo_in (f := f).
-Definition inj_homo_ltr_in :
-  {in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} ->
-  {in D & D', {homo f : x y / x < y}} :=
-  inj_homo_lt_in (f := f).
-Definition inj_nhomo_ltr_in :
-    {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} ->
-  {in D & D', {homo f : x y /~ x < y}} :=
-  inj_nhomo_lt_in (f := f).
-Definition incr_inj_in :
-  {in D &, {mono f : x y / x <= y}} -> {in D &, injective f} :=
-  inc_inj_in (f := f).
-Definition decr_inj_in :
-  {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f} :=
-  dec_inj_in (f := f).
-Definition lerW_mono_in :
-  {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}} :=
-  leW_mono_in (f := f).
-Definition lerW_nmono_in :
-  {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}} :=
-  leW_nmono_in (f := f).
-End AcrossTypes.
-Section NatToR.
-Variables (D D' : pred nat) (f : nat -> R).
-Definition ltnrW_homo :
-  {homo f : m n / (m < n)%N >-> m < n} ->
-  {homo f : m n / (m <= n)%N >-> m <= n} :=
-  ltW_homo (f := f).
-Definition ltnrW_nhomo :
-  {homo f : m n / (n < m)%N >-> m < n} ->
-  {homo f : m n / (n <= m)%N >-> m <= n} :=
-  ltW_nhomo (f := f).
-Definition inj_homo_ltnr : injective f ->
-  {homo f : m n / (m <= n)%N >-> m <= n} ->
-  {homo f : m n / (m < n)%N >-> m < n} :=
-  inj_homo_lt (f := f).
-Definition inj_nhomo_ltnr : injective f ->
-  {homo f : m n / (n <= m)%N >-> m <= n} ->
-  {homo f : m n / (n < m)%N >-> m < n} :=
-  inj_nhomo_lt (f := f).
-Definition incnr_inj :
-  {mono f : m n / (m <= n)%N >-> m <= n} -> injective f :=
-  inc_inj (f := f).
-Definition decnr_inj :
-  {mono f : m n / (n <= m)%N >-> m <= n} -> injective f :=
-  dec_inj (f := f).
-Definition decnr_inj_inj := decnr_inj.
-Definition lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} ->
-  {mono f : m n / (m < n)%N >-> m < n} :=
-  leW_mono (f := f).
-Definition lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} ->
-  {mono f : m n / (n < m)%N >-> m < n} :=
-  leW_nmono (f := f).
-Definition lenr_mono : {homo f : m n / (m < n)%N >-> m < n} ->
-   {mono f : m n / (m <= n)%N >-> m <= n} :=
-  le_mono (f := f).
-Definition lenr_nmono :
-  {homo f : m n / (n < m)%N >-> m < n} ->
-  {mono f : m n / (n <= m)%N >-> m <= n} :=
-  le_nmono (f := f).
-Definition ltnrW_homo_in :
-  {in D & D', {homo f : m n / (m < n)%N >-> m < n}} ->
-  {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} :=
-  ltW_homo_in (f := f).
-Definition ltnrW_nhomo_in :
-  {in D & D', {homo f : m n / (n < m)%N >-> m < n}} ->
-  {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} :=
-  ltW_nhomo_in (f := f).
-Definition inj_homo_ltnr_in : {in D & D', injective f} ->
-  {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} ->
-  {in D & D', {homo f : m n / (m < n)%N >-> m < n}} :=
-  inj_homo_lt_in (f := f).
-Definition inj_nhomo_ltnr_in : {in D & D', injective f} ->
-  {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} ->
-  {in D & D', {homo f : m n / (n < m)%N >-> m < n}} :=
-  inj_nhomo_lt_in (f := f).
-Definition incnr_inj_in :
-  {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> {in D &, injective f} :=
-  inc_inj_in (f := f).
-Definition decnr_inj_in :
-  {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> {in D &, injective f} :=
-  dec_inj_in (f := f).
-Definition decnr_inj_inj_in := decnr_inj_in.
-Definition lenrW_mono_in :
-  {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} ->
-  {in D &, {mono f : m n / (m < n)%N >-> m < n}} :=
-  leW_mono_in (f := f).
-Definition lenrW_nmono_in :
-  {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} ->
-  {in D &, {mono f : m n / (n < m)%N >-> m < n}} :=
-  leW_nmono_in (f := f).
-Definition lenr_mono_in :
-  {in D &, {homo f : m n / (m < n)%N >-> m < n}} ->
-  {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} :=
-  le_mono_in (f := f).
-Definition lenr_nmono_in :
-  {in D &, {homo f : m n / (n < m)%N >-> m < n}} ->
-  {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} :=
-  le_nmono_in (f := f).
-End NatToR.
-Section RToNat.
-Variables (D D' : pred R) (f : R -> nat).
-Definition ltrnW_homo :
-  {homo f : m n / m < n >-> (m < n)%N} ->
-  {homo f : m n / m <= n >-> (m <= n)%N} :=
-  ltW_homo (f := f).
-Definition ltrnW_nhomo :
-  {homo f : m n / n < m >-> (m < n)%N} ->
- {homo f : m n / n <= m >-> (m <= n)%N} :=
-  ltW_nhomo (f := f).
-Definition inj_homo_ltrn : injective f ->
-  {homo f : m n / m <= n >-> (m <= n)%N} ->
-  {homo f : m n / m < n >-> (m < n)%N} :=
-  inj_homo_lt (f := f).
-Definition inj_nhomo_ltrn : injective f ->
-  {homo f : m n / n <= m >-> (m <= n)%N} ->
-  {homo f : m n / n < m >-> (m < n)%N} :=
-  inj_nhomo_lt (f := f).
-Definition incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f :=
-  inc_inj (f := f).
-Definition decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f :=
-  dec_inj (f := f).
-Definition lernW_mono :
-  {mono f : m n / m <= n >-> (m <= n)%N} ->
-  {mono f : m n / m < n >-> (m < n)%N} :=
-  leW_mono (f := f).
-Definition lernW_nmono :
-  {mono f : m n / n <= m >-> (m <= n)%N} ->
-  {mono f : m n / n < m >-> (m < n)%N} :=
-  leW_nmono (f := f).
-Definition ltrnW_homo_in :
-  {in D & D', {homo f : m n / m < n >-> (m < n)%N}} ->
-  {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} :=
-  ltW_homo_in (f := f).
-Definition ltrnW_nhomo_in :
-  {in D & D', {homo f : m n / n < m >-> (m < n)%N}} ->
-  {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} :=
-  ltW_nhomo_in (f := f).
-Definition inj_homo_ltrn_in : {in D & D', injective f} ->
-  {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} ->
-  {in D & D', {homo f : m n / m < n >-> (m < n)%N}} :=
-  inj_homo_lt_in (f := f).
-Definition inj_nhomo_ltrn_in : {in D & D', injective f} ->
-  {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} ->
-  {in D & D', {homo f : m n / n < m >-> (m < n)%N}} :=
-  inj_nhomo_lt_in (f := f).
-Definition incrn_inj_in :
-  {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> {in D &, injective f} :=
-  inc_inj_in (f := f).
-Definition decrn_inj_in :
-  {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> {in D &, injective f} :=
-  dec_inj_in (f := f).
-Definition lernW_mono_in :
-  {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} ->
-  {in D &, {mono f : m n / m < n >-> (m < n)%N}} :=
-  leW_mono_in (f := f).
-Definition lernW_nmono_in :
-  {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} ->
-  {in D &, {mono f : m n / n < m >-> (m < n)%N}} :=
-  leW_nmono_in (f := f).
-End RToNat.
-End NumIntegralDomainMonotonyTheory.
-
-Section NumDomainOperationTheory.
-Variable R : numDomainType.
-Implicit Types x y z t : R.
-Definition lerif_refl x C : reflect (x <= x ?= iff C) C := leif_refl.
-Definition lerif_trans x1 x2 x3 C12 C23 :
-  x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23 :=
-  @leif_trans _ _ x1 x2 x3 C12 C23.
-Definition lerif_le x y : x <= y -> x <= y ?= iff (x >= y) := @leif_le _ _ x y.
-Definition lerif_eq x y : x <= y -> x <= y ?= iff (x == y) := @leif_eq _ _ x y.
-Definition ger_lerif x y C : x <= y ?= iff C -> (y <= x) = C :=
-  @ge_leif _ _ x y C.
-Definition ltr_lerif x y C : x <= y ?= iff C -> (x < y) = ~~ C :=
-  @lt_leif _ _ x y C.
-Definition normr_real x : `|x| \is real := normr_real x.
-Definition ler_norm_sum I r (G : I -> R) (P : pred I):
-  `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i| :=
-  ler_norm_sum r G P.
-Definition ler_norm_sub x y : `|x - y| <= `|x| + `|y| := ler_norm_sub x y.
-Definition ler_dist_add z x y : `|x - y| <= `|x - z| + `|z - y| :=
-  ler_dist_add z x y.
-Definition ler_sub_norm_add x y : `|x| - `|y| <= `|x + y| :=
-  ler_sub_norm_add x y.
-Definition ler_sub_dist x y : `|x| - `|y| <= `|x - y| := ler_sub_dist x y.
-Definition ler_dist_dist x y : `| `|x| - `|y| | <= `|x - y| :=
-  ler_dist_dist x y.
-Definition ler_dist_norm_add x y : `| `|x| - `|y| | <= `|x + y| :=
-  ler_dist_norm_add x y.
-Definition ler_nnorml x y : y < 0 -> `|x| <= y = false := @ler_nnorml _ _ x y.
-Definition ltr_nnorml x y : y <= 0 -> `|x| < y = false := @ltr_nnorml _ _ x y.
-Definition lter_nnormr := (ler_nnorml, ltr_nnorml).
-Definition mono_in_lerif (A : pred R) (f : R -> R) C :
-  {in A &, {mono f : x y / x <= y}} ->
-  {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)} :=
-  @mono_in_leif _ _ A f C.
-Definition mono_lerif (f : R -> R) C :
-  {mono f : x y / x <= y} ->
-  forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C) :=
-  @mono_leif _ _ f C.
-Definition nmono_in_lerif (A : pred R) (f : R -> R) C :
-  {in A &, {mono f : x y /~ x <= y}} ->
-  {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)} :=
-  @nmono_in_leif _ _ A f C.
-Definition nmono_lerif (f : R -> R) C :
-  {mono f : x y /~ x <= y} ->
-  forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C) :=
-  @nmono_leif _ _ f C.
-End NumDomainOperationTheory.
-
-Section RealDomainTheory.
-Variable R : realDomainType.
-Implicit Types x y z t : R.
-Definition ler_total : total (@ler R) := le_total.
-Definition ltr_total x y : x != y -> (x < y) || (y < x) :=
-  @lt_total _ _ x y.
-Definition wlog_ler P :
-  (forall a b, P b a -> P a b) -> (forall a b, a <= b -> P a b) ->
-  forall a b : R, P a b :=
-  @wlog_le _ _ P.
-Definition wlog_ltr P :
-  (forall a, P a a) ->
-  (forall a b, (P b a -> P a b)) -> (forall a b, a < b -> P a b) ->
-  forall a b : R, P a b :=
-  @wlog_lt _ _ P.
-Definition ltrNge x y : (x < y) = ~~ (y <= x) := @ltNge _ _ x y.
-Definition lerNgt x y : (x <= y) = ~~ (y < x) := @leNgt _ _ x y.
-Definition neqr_lt x y : (x != y) = (x < y) || (y < x) := @neq_lt _ _ x y.
-Definition eqr_leLR x y z t :
-  (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t) :=
-  @eq_leLR _ _ x y z t.
-Definition eqr_leRL x y z t :
-  (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y) :=
-  @eq_leRL _ _ x y z t.
-Definition eqr_ltLR x y z t :
-  (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t) :=
-  @eq_ltLR _ _ x y z t.
-Definition eqr_ltRL x y z t :
-  (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y) :=
-  @eq_ltRL _ _ x y z t.
-End RealDomainTheory.
-
-Section RealDomainMonotony.
-Variables (R : realDomainType) (R' : numDomainType) (D : pred R).
-Variables (f : R -> R') (f' : R -> nat).
-Definition ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y} :=
-  le_mono (f := f).
-Definition homo_mono := ler_mono.
-Definition ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y} :=
-  le_nmono (f := f).
-Definition nhomo_mono := ler_nmono.
-Definition ler_mono_in :
-  {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}} :=
-  le_mono_in (f := f).
-Definition homo_mono_in := ler_mono_in.
-Definition ler_nmono_in :
-  {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}} :=
-  le_nmono_in (f := f).
-Definition nhomo_mono_in := ler_nmono_in.
-Definition lern_mono :
-  {homo f' : m n / m < n >-> (m < n)%N} ->
-  {mono f' : m n / m <= n >-> (m <= n)%N} :=
-  le_mono (f := f').
-Definition lern_nmono :
-  {homo f' : m n / n < m >-> (m < n)%N} ->
-  {mono f' : m n / n <= m >-> (m <= n)%N} :=
-  le_nmono (f := f').
-Definition lern_mono_in :
-  {in D &, {homo f' : m n / m < n >-> (m < n)%N}} ->
-  {in D &, {mono f' : m n / m <= n >-> (m <= n)%N}} :=
-  le_mono_in (f := f').
-Definition lern_nmono_in :
-  {in D &, {homo f' : m n / n < m >-> (m < n)%N}} ->
-  {in D &, {mono f' : m n / n <= m >-> (m <= n)%N}} :=
-  le_nmono_in (f := f').
-End RealDomainMonotony.
-
-Section RealDomainOperations.
-Variable R : realDomainType.
-Implicit Types x y z : R.
-Section MinMax.
-
-Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type.
-Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed.
-Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?].
-Ltac mexact x := by mapply x.
-
-Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed.
-Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed.
-Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed.
-Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed.
-Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed.
-Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed.
-Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed.
-Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed.
-
-Lemma minrA x y z : min x (min y z) = min (min x y) z.
-Proof. mexact @minA. Qed.
-
-Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed.
-Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed.
-Lemma maxrA x y z : max x (max y z) = max (max x y) z.
-Proof. mexact @maxA. Qed.
-
-Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed.
-Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed.
-Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed.
-Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed.
-Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed.
-Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed.
-
-Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z).
-Proof. mexact @le_minr. Qed.
-
-Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x).
-Proof. mexact @le_minl. Qed.
-
-Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z).
-Proof. mexact @le_maxr. Qed.
-
-Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x).
-Proof. mexact @le_maxl. Qed.
-
-Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z).
-Proof. mexact @lt_minr. Qed.
-
-Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x).
-Proof. mexact @lt_minl. Qed.
-
-Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z).
-Proof. mexact @lt_maxr. Qed.
-
-Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x).
-Proof. mexact @lt_maxl. Qed.
-
-Definition lter_minr := (ler_minr, ltr_minr).
-Definition lter_minl := (ler_minl, ltr_minl).
-Definition lter_maxr := (ler_maxr, ltr_maxr).
-Definition lter_maxl := (ler_maxl, ltr_maxl).
-
-Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed.
-Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed.
-
-Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed.
-Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed.
-Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed.
-Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed.
-
-Variant minr_spec x y : bool -> bool -> R -> Type :=
-| Minr_r of x <= y : minr_spec x y true false x
-| Minr_l of y < x : minr_spec x y false true y.
-Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y).
-Proof. by rewrite mrE; case: leP; constructor. Qed.
-
-Variant maxr_spec x y : bool -> bool -> R -> Type :=
-| Maxr_r of y <= x : maxr_spec x y true false x
-| Maxr_l of x < y : maxr_spec x y false true y.
-Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y).
-Proof. by rewrite mrE; case: (leP y); constructor. Qed.
-
-End MinMax.
-End RealDomainOperations.
-
-Arguments lerifP {R x y C}.
-Arguments lerif_refl {R x C}.
-Arguments mono_in_lerif [R A f C].
-Arguments nmono_in_lerif [R A f C].
-Arguments mono_lerif [R f C].
-Arguments nmono_lerif [R f C].
-
-Section RealDomainArgExtremum.
-
-Context {R : realDomainType} {I : finType} (i0 : I).
-Context (P : pred I) (F : I -> R) (Pi0 : P i0).
-
-Definition arg_minr := extremum <=%R i0 P F.
-Definition arg_maxr := extremum >=%R i0 P F.
-Definition arg_minrP : extremum_spec <=%R P F arg_minr := arg_minP F Pi0.
-Definition arg_maxrP : extremum_spec >=%R P F arg_maxr := arg_maxP F Pi0.
-
-End RealDomainArgExtremum.
-
-Notation "@ 'real_lerP'" :=
-  (deprecate real_lerP real_leP) (at level 10, only parsing) : fun_scope.
-Notation real_lerP := (@real_lerP _ _ _) (only parsing).
-Notation "@ 'real_ltrP'" :=
-  (deprecate real_ltrP real_ltP) (at level 10, only parsing) : fun_scope.
-Notation real_ltrP := (@real_ltrP _ _ _) (only parsing).
-Notation "@ 'real_ltrNge'" :=
-  (deprecate real_ltrNge real_ltNge) (at level 10, only parsing) : fun_scope.
-Notation real_ltrNge := (@real_ltrNge _ _ _) (only parsing).
-Notation "@ 'real_lerNgt'" :=
-  (deprecate real_lerNgt real_leNgt) (at level 10, only parsing) : fun_scope.
-Notation real_lerNgt := (@real_lerNgt _ _ _) (only parsing).
-Notation "@ 'real_ltrgtP'" :=
-  (deprecate real_ltrgtP real_ltgtP) (at level 10, only parsing) : fun_scope.
-Notation real_ltrgtP := (@real_ltrgtP _ _ _) (only parsing).
-Notation "@ 'real_ger0P'" :=
-  (deprecate real_ger0P real_ge0P) (at level 10, only parsing) : fun_scope.
-Notation real_ger0P := (@real_ger0P _ _) (only parsing).
-Notation "@ 'real_ltrgt0P'" :=
-  (deprecate real_ltrgt0P real_ltgt0P) (at level 10, only parsing) : fun_scope.
-Notation real_ltrgt0P := (@real_ltrgt0P _ _) (only parsing).
-Notation lerif_nat := (deprecate lerif_nat leif_nat_r) (only parsing).
-Notation "@ 'lerif_subLR'" :=
-  (deprecate lerif_subLR leif_subLR) (at level 10, only parsing) : fun_scope.
-Notation lerif_subLR := (@lerif_subLR _) (only parsing).
-Notation "@ 'lerif_subRL'" :=
-  (deprecate lerif_subRL leif_subRL) (at level 10, only parsing) : fun_scope.
-Notation lerif_subRL := (@lerif_subRL _) (only parsing).
-Notation "@ 'lerif_add'" :=
-  (deprecate lerif_add leif_add) (at level 10, only parsing) : fun_scope.
-Notation lerif_add := (@lerif_add _ _ _ _ _ _ _) (only parsing).
-Notation "@ 'lerif_sum'" :=
-  (deprecate lerif_sum leif_sum) (at level 10, only parsing) : fun_scope.
-Notation lerif_sum := (@lerif_sum _ _ _ _ _ _) (only parsing).
-Notation "@ 'lerif_0_sum'" :=
-  (deprecate lerif_0_sum leif_0_sum) (at level 10, only parsing) : fun_scope.
-Notation lerif_0_sum := (@lerif_0_sum _ _ _ _ _) (only parsing).
-Notation "@ 'real_lerif_norm'" :=
-  (deprecate real_lerif_norm real_leif_norm)
-  (at level 10, only parsing) : fun_scope.
-Notation real_lerif_norm := (@real_lerif_norm _ _) (only parsing).
-Notation "@ 'lerif_pmul'" :=
-  (deprecate lerif_pmul leif_pmul) (at level 10, only parsing) : fun_scope.
-Notation lerif_pmul := (@lerif_pmul _ _ _ _ _ _ _) (only parsing).
-Notation "@ 'lerif_nmul'" :=
-  (deprecate lerif_nmul leif_nmul) (at level 10, only parsing) : fun_scope.
-Notation lerif_nmul := (@lerif_nmul _ _ _ _ _ _ _) (only parsing).
-Notation "@ 'lerif_pprod'" :=
-  (deprecate lerif_pprod leif_pprod) (at level 10, only parsing) : fun_scope.
-Notation lerif_pprod := (@lerif_pprod _ _ _ _ _ _) (only parsing).
-Notation "@ 'real_lerif_mean_square_scaled'" :=
-  (deprecate real_lerif_mean_square_scaled real_leif_mean_square_scaled)
-  (at level 10, only parsing) : fun_scope.
-Notation real_lerif_mean_square_scaled :=
-  (@real_lerif_mean_square_scaled _ _ _ _ _ _) (only parsing).
-Notation "@ 'real_lerif_AGM2_scaled'" :=
-  (deprecate real_lerif_AGM2_scaled real_leif_AGM2_scaled)
-  (at level 10, only parsing) : fun_scope.
-Notation real_lerif_AGM2_scaled :=
-  (@real_lerif_AGM2_scaled _ _ _) (only parsing).
-Notation "@ 'lerif_AGM_scaled'" :=
-  (deprecate lerif_AGM_scaled leif_AGM2_scaled)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_AGM_scaled := (@lerif_AGM_scaled _ _ _ _) (only parsing).
-Notation "@ 'real_lerif_mean_square'" :=
-  (deprecate real_lerif_mean_square real_leif_mean_square)
-  (at level 10, only parsing) : fun_scope.
-Notation real_lerif_mean_square :=
-  (@real_lerif_mean_square _ _ _) (only parsing).
-Notation "@ 'real_lerif_AGM2'" :=
-  (deprecate real_lerif_AGM2 real_leif_AGM2)
-  (at level 10, only parsing) : fun_scope.
-Notation real_lerif_AGM2 := (@real_lerif_AGM2 _ _ _) (only parsing).
-Notation "@ 'lerif_AGM'" :=
-  (deprecate lerif_AGM leif_AGM) (at level 10, only parsing) : fun_scope.
-Notation lerif_AGM := (@lerif_AGM _ _ _ _) (only parsing).
-Notation "@ 'lerif_mean_square_scaled'" :=
-  (deprecate lerif_mean_square_scaled leif_mean_square_scaled)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_mean_square_scaled :=
-  (@lerif_mean_square_scaled _) (only parsing).
-Notation "@ 'lerif_AGM2_scaled'" :=
-  (deprecate lerif_AGM2_scaled leif_AGM2_scaled)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_AGM2_scaled := (@lerif_AGM2_scaled _) (only parsing).
-Notation "@ 'lerif_mean_square'" :=
-  (deprecate lerif_mean_square leif_mean_square)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_mean_square := (@lerif_mean_square _) (only parsing).
-Notation "@ 'lerif_AGM2'" :=
-  (deprecate lerif_AGM2 leif_AGM2) (at level 10, only parsing) : fun_scope.
-Notation lerif_AGM2 := (@lerif_AGM2 _) (only parsing).
-Notation "@ 'lerif_normC_Re_Creal'" :=
-  (deprecate lerif_normC_Re_Creal leif_normC_Re_Creal)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_normC_Re_Creal := (@lerif_normC_Re_Creal _) (only parsing).
-Notation "@ 'lerif_Re_Creal'" :=
-  (deprecate lerif_Re_Creal leif_Re_Creal)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_Re_Creal := (@lerif_Re_Creal _) (only parsing).
-Notation "@ 'lerif_rootC_AGM'" :=
-  (deprecate lerif_rootC_AGM leif_rootC_AGM)
-  (at level 10, only parsing) : fun_scope.
-Notation lerif_rootC_AGM := (@lerif_rootC_AGM _ _ _ _) (only parsing).
-
-End Theory.
-
-Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" :=
-    (arg_minr i0 (fun i => P%B) (fun i => F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'minr_' ( i  <  i0  |  P )  F ]") : form_scope.
-
-Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" :=
-    [arg minr_(i < i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'minr_' ( i  <  i0  'in'  A )  F ]") : form_scope.
-
-Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'minr_' ( i  <  i0 )  F ]") : form_scope.
-
-Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" :=
-     (arg_maxr i0 (fun i => P%B) (fun i => F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'maxr_' ( i  >  i0  |  P )  F ]") : form_scope.
-
-Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" :=
-    [arg maxr_(i > i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'maxr_' ( i  >  i0  'in'  A )  F ]") : form_scope.
-
-Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'maxr_' ( i  >  i0 ) F ]") : form_scope.
-
-End Num.
-End mc_1_10.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 76bec6f..7875323 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -2049,6 +2049,5 @@ Qed.
 
 End Solver.
 
-Notation "@ 'limg_add'" :=
-  (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope.
-Notation limg_add := (@limg_add _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use limgD instead.")]
+Notation limg_add := limgD (only parsing).
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 17b1490..64863f4 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2490,7 +2490,5 @@ Definition conj_cfMod := cfAutMod conjC.
 Definition conj_cfInd := cfAutInd conjC.
 Definition cfconjC_eq1 := cfAut_eq1 conjC.
 
-Notation "@ 'cf_triangle_lerif'" :=
-  (deprecate cf_triangle_lerif cf_triangle_leif)
-  (at level 10, only parsing).
-Notation cf_triangle_lerif := (@cf_triangle_lerif _ _) (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use cf_triangle_leif instead.")]
+Notation cf_triangle_lerif := cf_triangle_leif (only parsing).
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).
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index c1f420f..10c0849 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -453,12 +453,10 @@ Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).
 
 End Theory.
 
-Notation "@ 'mulm_addl'" :=
-  (deprecate mulm_addl mulmDl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'mulm_addr'" :=
-  (deprecate mulm_addr mulmDr) (at level 10, only parsing) : fun_scope.
-Notation mulm_addl := (@mulm_addl _ _ _) (only parsing).
-Notation mulm_addr := (@mulm_addr _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mulmDl instead.")]
+Notation mulm_addl := mulmDl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mulmDr instead.")]
+Notation mulm_addr := mulmDr (only parsing).
 
 End Theory.
 Include Theory.
@@ -1991,14 +1989,9 @@ 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 filter_index_enum :=
-  ((fun _ => @deprecated_filter_index_enum _)
-     (deprecate filter_index_enum big_enumP)) (only parsing).
-
-Notation big_rmcond :=
-  ((fun _ _ _ _ => @big_rmcond_in _ _ _ _)
-     (deprecate big_rmcond big_rmcond_in)) (only parsing).
-
-Notation big_uncond_in :=
-  ((fun _ _ _ _ => @big_rmcond_in _ _ _ _)
-     (deprecate big_uncond_in big_rmcond_in)) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use big_enumP instead.")]
+Notation filter_index_enum := deprecated_filter_index_enum (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use big_rmcond_in instead.")]
+Notation big_rmcond := big_rmcond_in (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use big_rmcond_in instead.")]
+Notation big_uncond_in := big_rmcond_in (only parsing).
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index ae46cd3..aca1a29 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -1041,11 +1041,11 @@ Qed.
 
 End Chinese.
 
-Notation "@ 'coprime_expl'" :=
-  (deprecate coprime_expl coprimeXl) (at level 10, only parsing) : fun_scope.
-Notation "@ 'coprime_expr'" :=
-  (deprecate coprime_expr coprimeXr) (at level 10, only parsing) : fun_scope.
-Notation coprime_mull := (deprecate coprime_mull coprimeMl) (only parsing).
-Notation coprime_mulr := (deprecate coprime_mulr coprimeMr) (only parsing).
-Notation coprime_expl := (fun k => @coprime_expl k _ _) (only parsing).
-Notation coprime_expr := (fun k => @coprime_expr k _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimeMl instead.")]
+Notation coprime_mull := coprimeMl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimeMr instead.")]
+Notation coprime_mulr := coprimeMr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimeXl instead.")]
+Notation coprime_expl := coprimeXl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use coprimeXr instead.")]
+Notation coprime_expr := coprimeXr (only parsing).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 027b5d4..f0e1f5e 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2357,9 +2357,7 @@ End Greatest.
 
 End SetFixpoint.
 
-Notation mem_imset := 
-  ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _)
-  (only parsing).
-Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => 
-  deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _)
-  (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use imset_f instead.")]
+Notation mem_imset := imset_f (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use imset2_f instead.")]
+Notation mem_imset2 := imset2_f (only parsing).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 9d2b6c0..4fc602c 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -917,8 +917,8 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed.
 
 End OpsTheory.
 
-Notation disjoint_trans := 
-  (deprecate disjoint_trans disjointWl _ _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use disjointWl instead.")]
+Notation disjoint_trans := disjointWl (only parsing).
 
 Hint Resolve subxx_hint : core.
 
@@ -1723,12 +1723,10 @@ End ArgMinMax.
 
 End Extrema.
 
-Notation "@ 'arg_minP'" :=
-  (deprecate arg_minP arg_minnP) (at level 10, only parsing) : fun_scope.
-Notation arg_minP := (@arg_minP _ _ _) (only parsing).
-Notation "@ 'arg_maxP'" :=
-  (deprecate arg_maxP arg_maxnP) (at level 10, only parsing) : fun_scope.
-Notation arg_maxP := (@arg_maxP _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use arg_minnP instead.")]
+Notation arg_minP := arg_minnP (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use arg_maxnP instead.")]
+Notation arg_maxP := arg_maxnP (only parsing).
 
 Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
     (arg_min i0 (fun i => P%B) (fun i => F))
@@ -2352,5 +2350,7 @@ Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed.
 
 End SumFinType.
 
-Notation bump_addl := (deprecate bump_addl bumpDl) (only parsing).
-Notation unbump_addl := (deprecate unbump_addl unbumpDl) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use bumpDl instead.")]
+Notation bump_addl := bumpDl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use unbumpDl instead.")]
+Notation unbump_addl := unbumpDl (only parsing).
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 5032dfd..24fb6f2 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -3422,12 +3422,10 @@ Proof. exact: anti_mono_in. Qed.
 
 End POrderMonotonyTheory.
 
-Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt lt_sorted_eq)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'eq_sorted_le'" := (deprecate eq_sorted_le le_sorted_eq)
-  (at level 10, only parsing) : fun_scope.
-Notation eq_sorted_lt := (@eq_sorted_lt _ _ _ _) (only parsing).
-Notation eq_sorted_le := (@eq_sorted_le _ _ _ _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use lt_sorted_eq instead.")]
+Notation eq_sorted_lt := lt_sorted_eq (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use le_sorted_eq instead.")]
+Notation eq_sorted_le := le_sorted_eq (only parsing).
 
 End POrderTheory.
 
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index d5c9488..dd3e867 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -1677,64 +1677,27 @@ End CycleArc.
 
 Prenex Implicits arc.
 
-(* Deprecated in 1.12.0 *)
-
-Notation "@ 'eq_sorted'" :=
-  (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope.
-Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'sorted_lt_nth'" :=
-  (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) =>
-     deprecate sorted_lt_nth sorted_ltn_nth leT_tr)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'sorted_le_nth'" :=
-  (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) =>
-     deprecate sorted_le_nth sorted_leq_nth leT_tr)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'ltn_index'" :=
-  (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) =>
-     deprecate ltn_index sorted_ltn_index leT_tr)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'leq_index'" :=
-  (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) =>
-     deprecate leq_index sorted_leq_index leT_tr)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'subseq_order_path'" := (deprecate subseq_order_path subseq_path)
-  (at level 10, only parsing) : fun_scope.
-
-Notation eq_sorted :=
-  (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing).
-Notation eq_sorted_irr :=
-  (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing).
-Notation sorted_lt_nth :=
-  (fun leT_tr x0 => @sorted_lt_nth _ _ leT_tr x0 _) (only parsing).
-Notation sorted_le_nth :=
-  (fun leT_tr leT_refl x0 => @sorted_le_nth _ _ leT_tr leT_refl x0 _)
-  (only parsing).
-Notation ltn_index := (fun leT_tr => @ltn_index _ _ leT_tr _) (only parsing).
-Notation leq_index :=
-  (fun leT_tr leT_refl => @leq_index _ _ leT_tr leT_refl _) (only parsing).
-Notation subseq_order_path :=
-  (fun leT_tr => @subseq_order_path _ _ leT_tr _ _ _) (only parsing).
-
-(* Deprecated in 1.13.0 *)
-
-Notation "@ 'sub_path_in'" :=
-  (deprecate sub_path_in sub_in_path) (at level 10, only parsing) : fun_scope.
-Notation "@ 'sub_cycle_in'" :=
-  (deprecate sub_cycle_in sub_in_cycle) (at level 10, only parsing) : fun_scope.
-Notation "@ 'sub_sorted_in'" := (deprecate sub_sorted_in sub_in_sorted)
-  (at level 10, only parsing) : fun_scope.
-Notation "@ 'eq_path_in'" :=
-  (deprecate eq_path_in eq_in_path) (at level 10, only parsing) : fun_scope.
-Notation "@ 'eq_cycle_in'" :=
-  (deprecate eq_cycle_in eq_in_cycle) (at level 10, only parsing) : fun_scope.
-
-Notation sub_path_in :=
-  (fun ee' => @sub_path_in _ _ _ _ ee' _ _) (only parsing).
-Notation sub_cycle_in :=
-  (fun ee' => @sub_cycle_in _ _ _ _ ee' _) (only parsing).
-Notation sub_sorted_in :=
-  (fun ee' => @sub_sorted_in _ _ _ _ ee' _) (only parsing).
-Notation eq_path_in := (fun ee' => @eq_path_in _ _ _ _ ee' _ _) (only parsing).
-Notation eq_cycle_in := (fun ee' => @eq_cycle_in _ _ _ _ ee' _) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sorted_eq instead.")]
+Notation eq_sorted := sorted_eq (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use irr_sorted_eq instead.")]
+Notation eq_sorted_irr := irr_sorted_eq (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sorted_ltn_nth instead.")]
+Notation sorted_lt_nth := sorted_ltn_nth (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sorted_leq_nth instead.")]
+Notation sorted_le_nth := sorted_leq_nth (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sorted_ltn_index instead.")]
+Notation ltn_index := sorted_ltn_index (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sorted_leq_index instead.")]
+Notation leq_index := sorted_leq_index (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use subseq_path instead.")]
+Notation subseq_order_path := subseq_path (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_path instead.")]
+Notation sub_path_in := sub_in_path (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_cycle instead.")]
+Notation sub_cycle_in := sub_in_cycle (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_sorted instead.")]
+Notation sub_sorted_in := sub_in_sorted (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use eq_in_path instead.")]
+Notation eq_path_in := eq_in_path (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use eq_in_cycle instead.")]
+Notation eq_cycle_in := eq_in_cycle (only parsing).
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index ee5b136..f94e0a1 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -1429,11 +1429,11 @@ apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //.
 by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord.
 Qed.
 
-Notation "@ 'primes_mul'" :=
-  (deprecate primes_mul primesM) (at level 10, only parsing) : fun_scope.
-Notation "@ 'primes_exp'" :=
-  (deprecate primes_exp primesX) (at level 10, only parsing) : fun_scope.
-Notation primes_mul := (@primes_mul _ _) (only parsing).
-Notation primes_exp := (fun m => @primes_exp m _) (only parsing).
-Notation pnat_mul := (deprecate pnat_mul pnatM) (only parsing).
-Notation pnat_exp := (deprecate pnat_exp pnatX) (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use primesM instead.")]
+Notation primes_mul := primesM (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use primesX instead.")]
+Notation primes_exp := primesX (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use pnatM instead.")]
+Notation pnat_mul := pnatM (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use pnatX instead.")]
+Notation pnat_exp := pnatX (only parsing).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 2d5c5b8..e1e0ad4 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -4040,38 +4040,19 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
 Ltac tfae := do !apply: AllIffConj.
 
 (* Temporary backward compatibility. *)
-Notation take_addn := (deprecate take_addn takeD _) (only parsing).
-Notation rot_addn := (deprecate rot_addn rotD _) (only parsing).
-Notation nseq_addn := (deprecate nseq_addn nseqD _) (only parsing).
-Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
-  (only parsing).
-Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)
-  (only parsing).
-Notation perm_eq_all := (deprecate perm_eq_all perm_all _ _ _)
-  (only parsing).
-Notation perm_eq_small := (deprecate perm_eq_small perm_small_eq _ _ _)
-  (only parsing).
-Notation perm_eq_nilP := (deprecate perm_eq_nilP perm_nilP) (only parsing).
-Notation perm_eq_consP := (deprecate perm_eq_consP perm_consP) (only parsing).
-Notation leq_size_perm :=
-  ((fun T s1 s2 Us1 ss12 les21 =>
-   let: (Esz12, Es12) :=
-     deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21
-   in conj Es12 Esz12) _ _ _)
-  (only parsing).
-Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _)
-  (only parsing).
-Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing).
-Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _)
-  (only parsing).
-(* TODO: restore when Coq 8.10 is no longer supported                *)
-(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *)
+#[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.")]
+Notation rot_addn := rotD (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use nseqD instead.")]
+Notation nseq_addn := nseqD (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_catr instead.")]
+Notation allpairs_catr := mem_allpairs_catr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_consr instead.")]
+Notation allpairs_consr := mem_allpairs_consr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use allpairs_rconsr instead.")]
+Notation perm_allpairs_rconsr := allpairs_rconsr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use iotaDl instead.")]
+Notation iota_addl := iotaDl (only parsing).
+#[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")]
 Notation iota_add := iotaD (only parsing).
-Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing).
-
-Notation allpairs_catr :=
-  (deprecate allpairs_catr mem_allpairs_catr _ _ _) (only parsing).
-Notation allpairs_consr :=
-  (deprecate allpairs_consr mem_allpairs_consr _ _ _) (only parsing).
-Notation perm_allpairs_rconsr :=
-  (deprecate perm_allpairs_rconsr allpairs_rconsr _ _ _) (only parsing).
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index e1e1b71..faecce2 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -12,22 +12,6 @@ Global Set Bullet Behavior "None".
 (*                  Prop are canonical nonPropType instances. This is         *)
 (*                  useful for applied views.                                 *)
 (*   --> This will become standard with the Coq v8.11 SSReflect core library. *)
-(*  deprecate old new == new, but warning that old is deprecated and new      *)
-(*                       should be used instead.                              *)
-(*    --> Usage: Notation old := (deprecate old new) (only parsing).          *)
-(*    --> Caveat: deprecate old new only inherits new's maximal implicits;    *)
-(*        on-demand implicits should be added after : (deprecate old new _).  *)
-(*    --> Caveat 2: if premises or conclusions need to be adjusted, of for    *)
-(*        non-prenex implicits, use the idiom:                                *)
-(*         Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...)    *)
-(*                          _ _ ... _) (only printing).                       *)
-(*        where all the implicit a_i's occur first, and correspond to the     *)
-(*        trailing _'s, making sure deprecate old new is fully applied and    *)
-(*        there are _no implicits_ inside the (fun .. => ..) expression. This *)
-(*        is to avoid triggering a bug in SSReflect elaboration that is       *)
-(*        triggered by such evars under binders.                              *)
-(*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
-(*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
 (*                                                                            *)
 (*   Intro pattern ltac views:                                                *)
 (*   - top of the stack actions:                                              *)
@@ -95,6 +79,8 @@ Ltac flag old_id new_id :=
 Module Exports.
 Arguments hide {T} u v /.
 Coercion hide : exposed >-> hidden.
+#[deprecated(since="mathcomp 1.13.0",
+             note="Use the deprecated attribute instead.")]
 Notation deprecate old_id new_id :=
   (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id)
   (only parsing).
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8dbfc73..ad00d14 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1974,78 +1974,26 @@ Ltac nat_congr := first
      symmetry
    end ].
 
-Module mc_1_10.
-
-Variant leq_xor_gtn m n : bool -> bool -> Set :=
-  | LeqNotGtn of m <= n : leq_xor_gtn m n true false
-  | GtnNotLeq of n < m  : leq_xor_gtn m n false true.
-
-Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m).
-Proof. by case: leqP; constructor. Qed.
-
-Variant ltn_xor_geq m n : bool -> bool -> Set :=
-  | LtnNotGeq of m < n  : ltn_xor_geq m n false true
-  | GeqNotLtn of n <= m : ltn_xor_geq m n true false.
-
-Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n).
-Proof. by case: ltnP; constructor. Qed.
-
-Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
-  | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
-  | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
-
-Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
-Proof. by case: n; constructor. Qed.
-
-Variant compare_nat m n :
-   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
-  | CompareNatLt of m < n : compare_nat m n false false false true false true
-  | CompareNatGt of m > n : compare_nat m n false false true false true false
-  | CompareNatEq of m = n : compare_nat m n true true true true false false.
-
-Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m)
-                                   (m <= n) (n < m) (m < n).
-Proof. by case: ltngtP; constructor. Qed.
-
-End mc_1_10.
-
 (* Temporary backward compatibility. *)
-Notation odd_add := (deprecate odd_add oddD _) (only parsing).
-Notation odd_sub := (deprecate odd_sub oddB _) (only parsing).
-
-Notation "@ 'homo_inj_lt'" :=
-  (deprecate homo_inj_lt inj_homo_ltn) (at level 10, only parsing) : fun_scope.
-Notation homo_inj_lt := (@homo_inj_lt _) (only parsing).
-Notation "@ 'homo_inj_lt_in'" :=
-  (deprecate homo_inj_lt_in inj_homo_ltn_in) (at level 10, only parsing) : fun_scope.
-Notation homo_inj_lt_in := (@homo_inj_lt_in _ _ _) (only parsing).
-
-Notation "@ 'incr_inj'" :=
-  (deprecate incr_inj incn_inj) (at level 10, only parsing) : fun_scope.
-Notation incr_inj := (@incr_inj _) (only parsing).
-Notation "@ 'incr_inj_in'" :=
-  (deprecate incr_inj_in incn_inj_in) (at level 10, only parsing) : fun_scope.
-Notation incr_inj_in := (@incr_inj_in _ _) (only parsing).
-
-Notation "@ 'decr_inj'" :=
-  (deprecate decr_inj decn_inj) (at level 10, only parsing) : fun_scope.
-Notation decr_inj := (@decr_inj _) (only parsing).
-Notation "@ 'decr_inj_in'" :=
-  (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope.
-Notation decr_inj_in := (@decr_inj_in _ _) (only parsing).
-
-Notation "@ 'iter_add'" :=
-  (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope.
-Notation "@ 'odd_opp'" :=
-  (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope.
-Notation "@ 'sqrn_sub'" :=
-  (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope.
-Notation iter_add := (@iterD _) (only parsing).
-Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing).
-Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing).
-Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing).
-Notation minn_mull := (deprecate minn_mull minnMl) (only parsing).
-Notation odd_opp := (@odd_opp _ _) (only parsing).
-Notation odd_mul := (deprecate odd_mul oddM) (only parsing).
-Notation odd_exp := (deprecate odd_exp oddX) (only parsing).
-Notation sqrn_sub := (@sqrn_sub _ _) (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use oddD instead.")]
+Notation odd_add := oddD (only parsing).
+#[deprecated(since="mathcomp 1.11.0", note="Use oddB instead.")]
+Notation odd_sub := oddB (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use iterD instead.")]
+Notation iter_add := iterD (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use maxnMr instead.")]
+Notation maxn_mulr := maxnMr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use maxnMl instead.")]
+Notation maxn_mull := maxnMl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use minnMr instead.")]
+Notation minn_mulr := minnMr (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use minnMl instead.")]
+Notation minn_mull := minnMl (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use oddN instead.")]
+Notation odd_opp := oddN (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use oddM instead.")]
+Notation odd_mul := oddM (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use oddX instead.")]
+Notation odd_exp := oddX (only parsing).
+#[deprecated(since="mathcomp 1.12.0", note="Use sqrnB instead.")]
+Notation sqrn_sub := sqrnB (only parsing).