diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 27 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 20 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 85 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 49 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 18 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 96 |
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). |