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

Drop support for Coq 8.10

10 files changed, 247 insertions, 1158 deletions

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).