rm deprecated, reduce warnings

Author: affeldt-aist

classical/cardinality.v

@@ -742,8 +742,6 @@ move=> /finite_fsetP[{}A ->] /finite_fsetP[{}B ->].
 apply/finite_fsetP; exists (A `*` B)%fset; apply/predeqP => x.
 by split; rewrite /= inE => /andP.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setX.")]
-Notation finite_setM := finite_setX (only parsing).
 
 Lemma finite_image2 [aT bT rT : Type] [A : set aT] [B : set bT]
     (f : aT -> bT -> rT) :
@@ -843,8 +841,6 @@ apply/fsetP => i; apply/idP/idP; rewrite !(inE, in_fset_set)//=.
   by move=> [/mem_set-> /mem_set->].
 by move=> /andP[]; rewrite !inE.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fset_setX.")]
-Notation fset_setM := fset_setX (only parsing).
 
 Definition fst_fset (T1 T2 : choiceType) (A : {fset (T1 * T2)}) : {fset T1} :=
   [fset x.1 | x in A]%fset.
@@ -912,17 +908,13 @@ Proof.
 move=> Afin Bfin; rewrite -bigcupX1l.
 by apply: bigcup_finite => // i Ai; exact/finite_setX/Bfin.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXR.")]
-Notation finite_setMR := finite_setXR (only parsing).
 
 Lemma finite_setXL (T T' : choiceType) (A : T' -> set T) (B : set T') :
   (forall x, B x -> finite_set (A x)) -> finite_set B -> finite_set (A ``*` B).
 Proof.
 move=> Afin Bfin; rewrite -bigcupX1r.
 by apply: bigcup_finite => // i Ai; apply/finite_setX => //; exact: Afin.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXL.")]
-Notation finite_setML := finite_setXL (only parsing).
 
 Lemma fset_set_II n : fset_set `I_n = [fset val i | i in 'I_n]%fset.
 Proof.
@@ -1232,23 +1224,17 @@ have /ppcard_leP[f] := Bc i Ai; apply/pcard_geP/surjPex.
 exists (fun k => (i, f^-1%FUN k)) => -[_ j]/= [-> dj].
 by exists (f j) => //=; rewrite funK ?inE.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXR.")]
-Notation countableMR := countableXR (only parsing).
 
 Lemma countableX T1 T2 (D1 : set T1) (D2 : set T2) :
   countable D1 -> countable D2 -> countable (D1 `*` D2).
 Proof. by move=> D1c D2c; exact: countableXR (fun _ _ => D2c). Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableX.")]
-Notation countableM := countableX (only parsing).
 
 Lemma countableXL T T' (A : T' -> set T) (B : set T') :
   countable B -> (forall i, B i -> countable (A i)) -> countable (A ``*` B).
 Proof.
 move=> Bc Ac; rewrite -bigcupX1r; apply: bigcup_countable => // i Bi.
 by apply: countableX => //; exact: Ac.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXL.")]
-Notation countableML := countableXL (only parsing).
 
 Lemma infiniteXRl T T' (A : set T) (B : T -> set T') :
   infinite_set A -> (forall i, B i !=set0) -> infinite_set (A `*`` B).
@@ -1257,8 +1243,6 @@ move=> /infiniteP/pcard_geP[f] /(_ _)/cid-/all_sig[b Bb].
 apply/infiniteP/pcard_geP/surjPex; exists (fun x => f x.1).
 by move=> i iT; have [a Aa fa] := 'oinvP_f iT; exists (a, b a).
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to infiniteXRl.")]
-Notation infiniteMRl := infiniteXRl (only parsing).
 
 Lemma cardXR_eq_nat T T' (A : set T) (B : T -> set T') :
     (A #= [set: nat] -> (forall i, countable (B i) /\ B i !=set0) ->
@@ -1267,8 +1251,6 @@ Proof.
 rewrite !card_eq_le => /andP[Acnt /infiniteP Ainfty] /all_and2[Bcnt Bn0].
 by rewrite [(_ #<= _)%card]countableXR//=; exact/infiniteP/infiniteXRl.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to cardXR_eq_nat.")]
-Notation cardMR_eq_nat := cardXR_eq_nat (only parsing).
 
 Lemma eq_cardSP {T : Type} (A : set T) n :
   reflect (exists2 x, A x & A `\ x #= `I_n) (A #= `I_n.+1).

classical/classical_sets.v

@@ -337,14 +337,8 @@ Arguments setU _ _ _ _ /.
 Arguments setC _ _ _ /.
 Arguments setD _ _ _ _ /.
 Arguments setX _ _ _ _ _ /.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX.")]
-Notation setM := setX (only parsing).
 Arguments setXR _ _ _ _ _ /.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXR.")]
-Notation setMR := setXR (only parsing).
 Arguments setXL _ _ _ _ _ /.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXL.")]
-Notation setML := setXL (only parsing).
 Arguments fst_set _ _ _ _ /.
 Arguments snd_set _ _ _ _ /.
 Arguments subsetP {T A B}.
@@ -1189,33 +1183,7 @@ Arguments subsetT {T} A.
 
 #[global]
 Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use notin_setE instead.")]
-Notation notin_set := notin_setE (only parsing).
 Arguments setU_id2r {T} C {A B}.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_setX.")]
-Notation in_setM := in_setX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX0.")]
-Notation setM0 := setX0 (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to set0X.")]
-Notation set0M := set0X (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXTT.")]
-Notation setMTT := setXTT (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXT.")]
-Notation setMT := setXT (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setTX.")]
-Notation setTM := setTX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXI.")]
-Notation setMI := setXI (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupr.")]
-Notation setM_bigcupr := setX_bigcupr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupl.")]
-Notation setM_bigcupl := setX_bigcupl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setSX.")]
-Notation setSM := setSX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1l.")]
-Notation bigcupM1l := bigcupX1l (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1r.")]
-Notation bigcupM1r := bigcupX1r (only parsing).
 
 Lemma set_cst {T I} (x : T) (A : set I) :
   [set x | _ in A] = if A == set0 then set0 else [set x].
@@ -2090,11 +2058,6 @@ End bigop_lemmas.
 Arguments bigcup_setD1 {T I} x.
 Arguments bigcap_setD1 {T I} x.
 
-#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX_dep")]
-Notation bigcup_setM_dep := bigcup_setX_dep (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX")]
-Notation bigcup_setM := bigcup_setX (only parsing).
-
 Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j ->
   F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) =
   \bigcap_(i in P) F i.
@@ -3250,12 +3213,6 @@ Lemma fst_setXR (X : set T1) (Y : T1 -> set T2) : (X `*`` Y).`1 `<=` X.
 Proof. by move=> x [y [//]]. Qed.
 
 End product.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setX.")]
-Notation fst_setM := fst_setX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to snd_setX.")]
-Notation snd_setM := snd_setX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setXR instead.")]
-Notation fst_setMR := fst_setXR (only parsing).
 
 Section section.
 Variables (T1 T2 : Type).
@@ -3376,14 +3333,6 @@ Lemma ysection_preimage_fst (A : set T1) y : ysection (fst @^-1` A) y = A.
 Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed.
 
 End section.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_xsectionX.")]
-Notation in_xsectionM := in_xsectionX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_ysectionX.")]
-Notation in_ysectionM := in_ysectionX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_xsectionX.")]
-Notation notin_xsectionM := notin_xsectionX (only parsing).
-#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_ysectionX.")]
-Notation notin_ysectionM := notin_ysectionX (only parsing).
 
 Declare Scope relation_scope.
 Delimit Scope relation_scope with relation.

classical/fsbigop.v

@@ -1,6 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions cardinality.
 
 (**md**************************************************************************)

classical/functions.v

@@ -1,7 +1,9 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".

classical/mathcomp_extra.v

@@ -1,5 +1,5 @@
-(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect finmap ssralg ssrnum.
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -83,3 +83,15 @@ Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.
 Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
   #|` A| = (\sum_(i <- A) 1)%N.
 Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.
+
+(**************************)
+(* MathComp 2.6 additions *)
+(**************************)
+
+(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
+Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R.
+Proof. by rewrite intrD. Qed.
+
+(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
+Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R.
+Proof. by rewrite intrD. Qed.

classical/set_interval.v

@@ -1,7 +1,9 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions.
 
 (**md**************************************************************************)
@@ -208,8 +210,6 @@ Qed.
 
 End set_itv_porderType.
 Arguments neitv {disp T} _.
-#[deprecated(since="mathcomp-analysis 1.4.0", note="renamed to `subset_itvScc`")]
-Notation subset_itvS := subset_itvScc (only parsing).
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvNyy`")]
 Notation set_itv_infty_infty := set_itvNyy (only parsing).
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvoy`")]
@@ -707,7 +707,7 @@ Lemma range_factor ba bb a b : a < b ->
                  [set` Interval (BSide ba 0) (BSide bb 1)].
 Proof. by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.
 
-Lemma onem_factor a b x : a != b -> `1-(factor a b x) = factor b a x.
+Lemma onem_factor a b x : a != b -> (factor a b x).~ = factor b a x.
 Proof.
 rewrite eq_sym -subr_eq0 => ab; rewrite /onem /factor -(divff ab) -mulrBl.
 by rewrite opprB addrA subrK -mulrNN opprB -invrN opprB.

classical/unstable.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
-From mathcomp Require Import archimedean interval mathcomp_extra.
+From mathcomp Require Import archimedean interval.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -275,27 +275,31 @@ by rewrite (leq_trans (leq_card_setU _ _))// leq_add.
 Qed.
 
 Definition onem {R : pzRingType} (r : R) : R := 1 - r.
+#[deprecated(since="mathcomp-analysis 1.15.0")]
 Notation "`1- r" := (onem r) : ring_scope.
 
+Reserved Notation "p '.~'" (format "p .~", at level 1).
+Notation "p '.~'" := (onem p) : ring_scope.
+
 Section onem_ring.
 Context {R : pzRingType}.
 Implicit Type r : R.
 
-Lemma onem0 : `1-0 = 1 :> R. Proof. by rewrite /onem subr0. Qed.
+Lemma onem0 : 0.~ = 1 :> R. Proof. by rewrite /onem subr0. Qed.
 
-Lemma onem1 : `1-1 = 0 :> R. Proof. by rewrite /onem subrr. Qed.
+Lemma onem1 : 1.~ = 0 :> R. Proof. by rewrite /onem subrr. Qed.
 
-Lemma onemK r : `1-(`1-r) = r. Proof. exact: subKr. Qed.
+Lemma onemK r : (r.~).~ = r. Proof. exact: subKr. Qed.
 
-Lemma add_onemK r : r + `1- r = 1. Proof. by rewrite /onem addrC subrK. Qed.
+Lemma add_onemK r : r + r.~ = 1. Proof. by rewrite /onem addrC subrK. Qed.
 
-Lemma onemD r s : `1-(r + s) = `1-r - s.
+Lemma onemD r s : (r + s).~ = r.~ - s.
 Proof. by rewrite /onem opprD addrA. Qed.
 
-Lemma onemMr r s : s * `1-r = s - s * r.
+Lemma onemMr r s : s * r.~ = s - s * r.
 Proof. by rewrite /onem mulrBr mulr1. Qed.
 
-Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s.
+Lemma onemM r s : (r * s).~ = r.~ + s.~ - r.~ * s.~.
 Proof. by rewrite /onem mulrBl 2!mulrBr !mul1r mulr1 addrKA opprK subrKA. Qed.
 
 End onem_ring.
@@ -304,34 +308,34 @@ Section onem_order.
 Variable R : numDomainType.
 Implicit Types r : R.
 
-Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed.
+Lemma onem_gt0 r : r < 1 -> 0 < r.~. Proof. by rewrite subr_gt0. Qed.
 
-Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r.
+Lemma onem_ge0 r : r <= 1 -> 0 <= r.~.
 Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.
 
-Lemma onem_le1 r : 0 <= r -> `1-r <= 1.
+Lemma onem_le1 r : 0 <= r -> r.~ <= 1.
 Proof. by rewrite lerBlDr lerDl. Qed.
 
-Lemma onem_lt1 r : 0 < r -> `1-r < 1.
+Lemma onem_lt1 r : 0 < r -> r.~ < 1.
 Proof. by rewrite ltrBlDr ltrDl. Qed.
 
-Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n).
+Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= (r ^+ n).~.
 Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed.
 
-Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1.
+Lemma onemX_lt1 r n : 0 < r -> (r ^+ n).~ < 1.
 Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.
 
 End onem_order.
 
 Lemma normr_onem {R : realDomainType} (x : R) :
-  (0 <= x <= 1 -> `| `1-x | <= 1)%R.
+  (0 <= x <= 1 -> `| x.~ | <= 1)%R.
 Proof.
 move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split.
   by rewrite lerBrDl lerBlDr (le_trans x1)// lerDl.
 by rewrite lerBlDr lerDl.
 Qed.
 
-Lemma onemV (F : numFieldType) (x : F) : x != 0 -> `1-(x^-1) = (x - 1) / x.
+Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x.
 Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.
 
 Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.
@@ -401,14 +405,6 @@ Qed.
 
 End order_min.
 
-(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
-Lemma intrD1 {R : pzRingType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
-Proof. by rewrite intrD. Qed.
-
-(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
-Lemma intr1D {R : pzRingType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
-Proof. by rewrite intrD. Qed.
-
 Section bijection_forall.
 
 Lemma bij_forall A B (f : A -> B) (P : B -> Prop) :