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

Drop support for Coq 8.10

10 files changed, 107 insertions, 240 deletions

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