diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index dd3a74ea1..5a787419b 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1699,7 +1699,7 @@ Qed.
 End rectangle.
 
 Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT)
-    (G : set_system rT) : set (set aT) :=
+    (G : set_system rT) : set_system aT :=
   [set D `&` f @^-1` B | B in G].
 
 Lemma preimage_set_system0 {aT rT : Type} (D : set aT) (f : aT -> rT) :
@@ -1720,7 +1720,7 @@ apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
 by exists C => //; rewrite setTI comp_preimage.
 Qed.
 
-Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
+Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set_system aT) :
   preimage_set_system D idfun F = setI D @` F.
 Proof. by []. Qed.
 
@@ -1730,7 +1730,7 @@ Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
 Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
 
 Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
-    (G : set (set aT)) : set (set rT) :=
+    (G : set_system aT) : set_system rT :=
   [set B : set rT | G (D `&` f @^-1` B)].
 
 Section cross.
@@ -1746,15 +1746,15 @@ End cross.
 Definition cross12 {T1 T2 : Type} := @cross (T1 * T2)%type T1 T2 fst snd.
 Notation "A `x` B" := (cross12 A B) : classical_set_scope.
 
-Lemma subKimage {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
+Lemma subKimage {T T'} {P : set_system T'} (f : T -> T') (g : T' -> T) :
   cancel f g -> [set A | P (f @` A)] `<=` [set g @` A | A in P].
 Proof. by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.
 
-Lemma subimageK T T' (P : set (set T')) (f : T -> T') (g : T' -> T) :
+Lemma subimageK T T' (P : set_system T') (f : T -> T') (g : T' -> T) :
   cancel g f -> [set g @` A | A in P] `<=` [set A | P (f @` A)].
 Proof. by move=> gK _ [B /= ? <-]; rewrite image_comp eq_image_id/=. Qed.
 
-Lemma eq_imageK {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
+Lemma eq_imageK {T T'} {P : set_system T'} (f : T -> T') (g : T' -> T) :
     cancel f g -> cancel g f ->
   [set g @` A | A in P] = [set A | P (f @` A)].
 Proof.
@@ -3009,10 +3009,10 @@ Qed.
 End Zorn.
 
 Section Zorn_subset.
-Variables (T : Type) (P : set (set T)).
+Variables (T : Type) (P : set_system T).
 
 Lemma Zorn_bigcup :
-    (forall F : set (set T), F `<=` P -> total_on F subset ->
+    (forall F : set_system T, F `<=` P -> total_on F subset ->
       P (\bigcup_(X in F) X)) ->
   exists A, P A /\ forall B, A `<` B -> ~ P B.
 Proof.
@@ -3049,7 +3049,7 @@ Variables (B : I -> set T) (D : set I).
 
 Let P := fun X => X `<=` D /\ trivIset X B.
 
-Let maxP (A : set (set I)) :
+Let maxP (A : set_system I) :
   A `<=` P -> total_on A (fun x y => x `<=` y) -> P (\bigcup_(x in A) x).
 Proof.
 move=> AP h; split; first by apply: bigcup_sub => E /AP [].
@@ -3223,30 +3223,28 @@ rewrite -Order.TotalTheory.ltNge => kn.
 by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
 Qed.
 
-Definition meets T (F G : set (set T)) :=
+Definition meets T (F G : set_system T) :=
   forall A B, F A -> G B -> A `&` B !=set0.
 
 Notation "F `#` G" := (meets F G) : classical_set_scope.
 
 Section meets.
 
-Lemma meetsC T (F G : set (set T)) : F `#` G = G `#` F.
+Lemma meetsC T (F G : set_system T) : F `#` G = G `#` F.
 Proof.
 gen have sFG : F G / F `#` G -> G `#` F.
   by move=> FG B A => /FG; rewrite setIC; apply.
 by rewrite propeqE; split; apply: sFG.
 Qed.
 
-Lemma sub_meets T (F F' G G' : set (set T)) :
+Lemma sub_meets T (F F' G G' : set_system T) :
   F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G.
 Proof. by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed.
 
-Lemma meetsSr T (F G G' : set (set T)) :
-  G `<=` G' -> F `#` G' -> F `#` G.
+Lemma meetsSr T (F G G' : set_system T) : G `<=` G' -> F `#` G' -> F `#` G.
 Proof. exact: sub_meets. Qed.
 
-Lemma meetsSl T (G F F' : set (set T)) :
-  F `<=` F' -> F' `#` G -> F `#` G.
+Lemma meetsSl T (G F F' : set_system T) : F `<=` F' -> F' `#` G -> F `#` G.
 Proof. by move=> /sub_meets; apply. Qed.
 
 End meets.
diff --git a/classical/filter.v b/classical/filter.v
index 4eae1af6c..b26d00d72 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -1211,7 +1211,7 @@ Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
-  (F : set (set T)) (P : set T) :
+  (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->
   F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]).
 Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed.
@@ -1479,7 +1479,7 @@ End UltraFilters.
 
 Section filter_supremums.
 
-Global Instance smallest_filter_filter {T : Type} (F : set (set T)) :
+Global Instance smallest_filter_filter {T : Type} (F : set_system T) :
   Filter (smallest Filter F).
 Proof.
 split.
@@ -1488,13 +1488,13 @@ split.
 - by move=> ? ? /filterS + sFP ? [? ?]; apply; exact: sFP.
 Qed.
 
-Fixpoint filterI_iter {T : Type} (F : set (set T)) (n : nat) :=
+Fixpoint filterI_iter {T : Type} (F : set_system T) (n : nat) :=
   if n is m.+1
   then [set P `&` Q |
     P in filterI_iter F m & Q in filterI_iter F m]
   else setT |` F.
 
-Lemma filterI_iter_sub {T : Type} (F : set (set T)) :
+Lemma filterI_iter_sub {T : Type} (F : set_system T) :
   {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}.
 Proof.
 move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->.
@@ -1502,7 +1502,7 @@ move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|].
 by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid.
 Qed.
 
-Lemma filterI_iterE {T : Type} (F : set (set T)) :
+Lemma filterI_iterE {T : Type} (F : set_system T) :
   smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id.
 Proof.
 rewrite eqEsubset; split.
diff --git a/classical/functions.v b/classical/functions.v
index d60b235ce..3a98909ca 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -647,7 +647,8 @@ HB.instance Definition _ (f : {oinvfun A >-> B}) := Fun.on (oapp f).
 HB.instance Definition _ (f : {injfun A >-> B}) := Fun.on (oapp f).
 HB.instance Definition _ (f : {surjfun A >-> B}) := Fun.on (oapp f).
 HB.instance Definition _ (f : {bij A >-> B}) := Fun.on (oapp f).
-HB.instance Definition _ (f : {splitbij A >-> B}) := Fun.on (oapp f).
+(*HB.instance Definition _ (f : {splitbij A >-> B}) := Fun.on (oapp f).*)
+(* generates: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 End OApply.
 
diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v
index 47fa8630d..d1bc2ea08 100644
--- a/reals/prodnormedzmodule.v
+++ b/reals/prodnormedzmodule.v
@@ -21,13 +21,16 @@ Import Order.TTheory GRing.Theory Num.Theory.
 
 Section Linear1.
 Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
-HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.
-HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.
+(*HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.*)
+(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
+(*HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.*)
+(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
 End Linear1.
 Section Linear2.
 Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : GRing.Scale.law R V).
-HB.instance Definition _ :=
-  isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.
+(*HB.instance Definition _ :=
+  isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.*)
+(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
 End Linear2.
 
 Module ProdNormedZmodule.
diff --git a/theories/cantor.v b/theories/cantor.v
index 6a10eb7d4..f854cf6f2 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -397,7 +397,7 @@ Context (t0 t1 : T).
 Hypothesis T2e : t0 != t1.
 
 Let ent_balls' (E : set (T * T)) :
-  exists M : set (set T), entourage E -> [/\
+  exists M : set_system T, entourage E -> [/\
     finite_set M,
     forall A, M A -> exists a, A a /\
       A `<=` closure (xsection (split_ent E) a),
diff --git a/theories/derive.v b/theories/derive.v
index e4a340616..29542ad6f 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -69,7 +69,7 @@ Reserved Notation "f ^` ( n )" (format "f ^` ( n )").
 Section Differential.
 Context {K : numDomainType} {V W : normedModType K}.
 
-Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) :=
+Definition diff (F : filter_on V) (_ : phantom (set_system V) F) (f : V -> W) :=
   (get (fun (df : {linear V -> W}) => continuous df /\ forall x,
       f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).
 
@@ -77,14 +77,14 @@ Local Notation "''d' f x" := (@diff _ (Phantom _ (nbhs x)) f).
 
 Fact diff_key : forall T, T -> unit. Proof. by constructor. Qed.
 Variant differentiable_def (f : V -> W) (x : filter_on V)
-  (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of
+  (phF : phantom (set_system V) x) : Prop := DifferentiableDef of
   (continuous ('d f x) /\
   f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).
 
 Local Notation differentiable f F :=
   (@differentiable_def f _ (Phantom _ (nbhs F))).
 
-Class is_diff_def (x : filter_on V) (Fph : phantom (set (set V)) x) (f : V -> W)
+Class is_diff_def (x : filter_on V) (Fph : phantom (set_system V) x) (f : V -> W)
   (df : V -> W) := DiffDef {
     ex_diff : differentiable f x ;
     diff_val : 'd f x = df :> (V -> W)
diff --git a/theories/esum.v b/theories/esum.v
index 72d3ff110..3dc94ddbf 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -41,7 +41,7 @@ Section set_of_fset_in_a_set.
 Variable (T : choiceType).
 Implicit Type S : set T.
 
-Definition fsets S : set (set T) := [set F | finite_set F /\ F `<=` S].
+Definition fsets S : set_system T := [set F | finite_set F /\ F `<=` S].
 
 Lemma fsets_set0 S : fsets S set0. Proof. by split. Qed.
 
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 09354d098..003c63a01 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -939,7 +939,8 @@ HB.instance Definition _ :=
 Lemma LfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g.
 Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed.
 
-HB.instance Definition _ := [Choice of LfunType mu p1 by <:].
+(*HB.instance Definition _ := [Choice of LfunType mu p1 by <:].*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 Lemma finite_norm_cst0 : finite_norm mu p (cst 0).
 Proof. by rewrite /finite_norm Lnorm0// gt_eqF// (lt_le_trans _ p1). Qed.
diff --git a/theories/kernel.v b/theories/kernel.v
index 5c05838b9..7624108df 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -930,7 +930,7 @@ Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : pmeasurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R).
 Proof.
-apply: (measurability (@pset _ _ _ : set (set (pprobability Y R)))) => //.
+apply: (measurability (@pset _ _ _ : set_system (pprobability Y R))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-.
 rewrite /mnormalize /mset /preimage/=.
 apply: emeasurable_fun_infty_o => //.
diff --git a/theories/landau.v b/theories/landau.v
index 259f55d13..73c88b3a3 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -392,7 +392,7 @@ Lemma littleoE (tag : unit) (F : filter_on T)
 Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.
 
 Lemma littleoE0 (tag : unit) (F : filter_on T)
-   (phF : phantom (set (set T)) F) f h :
+   (phF : phantom (set_system T) F) f h :
    ~ littleo_def F f h -> the_littleo tag F phF f h = 0.
 Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed.
 
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
index 9486051ec..6803c75dc 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
@@ -373,8 +373,9 @@ split; first exact: measurableX.
 by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE.
 Qed.
 
-HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
-  product_measure_sigma_finite.
+(*HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
+  product_measure_sigma_finite.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 Lemma product_measure_unique
     (m' : {measure set (T1 * T2) -> \bar R}) :
@@ -390,7 +391,7 @@ have UFGT : \bigcup_k (F k `*` G k) = setT.
   move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
   - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
   - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
-pose C : set (set (T1 * T2)) :=
+pose C : set_system (T1 * T2) :=
   [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B].
 have CI : setI_closed C.
   move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]].
diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
index 21282d659..3c02ce4dd 100644
--- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v
+++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
@@ -381,12 +381,14 @@ Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).
 
 Import HBSimple.
 (* NB: already instantiated in cardinality.v *)
-HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).
+(*HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 Import HBNNSimple.
 (* NB: already instantiated in lebesgue_integral.v *)
-HB.instance Definition _ x : @NonNegFun T R (cst x%:num) :=
-  NonNegFun.on (cst x%:num).
+(*HB.instance Definition _ x : @NonNegFun T R (cst x%:num) :=
+  NonNegFun.on (cst x%:num).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 Lemma approximation_sfun :
   exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g ^~ x @ \oo --> f x).
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 778f5e20a..c82beeb32 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -177,7 +177,7 @@ HB.instance Definition _ :=
 End itv_semiRingOfSets.
 
 Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
-Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
+Notation "R .-ocitv.-measurable" := (measurable : set_system (ocitv_type R)) :
   classical_set_scope.
 
 Local Open Scope measure_display_scope.
@@ -519,9 +519,8 @@ Definition measurableTypeR (R : realType) :=
 Section lebesgue_stieltjes_measure.
 Context {R : realType}.
 
-Definition lebesgue_display : measure_display :=
-  (R.-ocitv.-measurable).-sigma.
-Definition measurableR : set (set R) :=
+Definition lebesgue_display : measure_display := (R.-ocitv.-measurable).-sigma.
+Definition measurableR : set_system R :=
   (R.-ocitv.-measurable).-sigma.-measurable.
 
 HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) :=
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index 28095e43e..002dcfe9e 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -93,10 +93,10 @@ Qed.
 End ps_infty.
 
 Section salgebra_ereal.
-Variables (R : realType) (G : set (set R)).
-Let measurableR : set (set R) := G.-sigma.-measurable.
+Variables (R : realType) (G : set_system R).
+Let measurableR : set_system R := G.-sigma.-measurable.
 
-Definition emeasurable : set (set \bar R) :=
+Definition emeasurable : set_system (\bar R) :=
   [set EFin @` A `|` B | A in measurableR & B in ps_infty].
 
 Lemma emeasurable0 : emeasurable set0.
@@ -418,7 +418,7 @@ Section rgencinfty.
 Variable R : realType.
 Implicit Types x y z : R.
 
-Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic].
+Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic].
 
 Lemma measurable_itv_bnd_infty b x :
   G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].
@@ -1184,7 +1184,7 @@ Module NGenCInfty.
 Section ngencinfty.
 Implicit Types x y z : nat.
 
-Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic].
+Definition G : set_system nat := [set A | exists x, A = `[x, +oo[%classic].
 
 Lemma measurable_itv_bnd_infty b x :
   G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].
diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v
index ea845e68e..91b1a9bcc 100644
--- a/theories/measure_theory/measurable_function.v
+++ b/theories/measure_theory/measurable_function.v
@@ -379,7 +379,7 @@ Lemma preimage_measurability d d' (aT : measurableType d)
 Proof. by move=> + mD Y mY; apply; exists Y. Qed.
 
 Lemma measurability d d' (aT : measurableType d) (rT : measurableType d')
-    (D : set aT) (f : aT -> rT) (G : set (set rT)) :
+    (D : set aT) (f : aT -> rT) (G : set_system rT) :
   @measurable _ rT = <<s G >> ->
   preimage_set_system D f G `<=` @measurable _ aT ->
   measurable_fun D f.
diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v
index 9512b6b6d..647d70f23 100644
--- a/theories/measure_theory/measurable_structure.v
+++ b/theories/measure_theory/measurable_structure.v
@@ -153,7 +153,7 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
 Section set_systems.
-Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)).
+Context {T} (C : set_system T -> Prop) (D : set T) (G : set_system T).
 
 Definition setC_closed := forall A, G A -> G (~` A).
 Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B).
@@ -250,7 +250,7 @@ Notation "'<<sr' G '>>'" := (smallest sigma_ring G) : classical_set_scope.
 Notation "'<<M' G '>>'" := (smallest monotone G) : classical_set_scope.
 
 Section lambda_system_smallest.
-Variables (T : Type) (D : set T) (G : set (set T)).
+Variables (T : Type) (D : set T) (G : set_system T).
 Hypothesis GD : forall A, G A -> A `<=` D.
 
 Lemma lambda_system_smallest : lambda_system D <<l D , G >>.
@@ -265,7 +265,7 @@ Qed.
 
 End lambda_system_smallest.
 
-Lemma fin_bigcup_closedP T (G : set (set T)) :
+Lemma fin_bigcup_closedP T (G : set_system T) :
   (G set0 /\ setU_closed G) <-> fin_bigcup_closed G.
 Proof.
 split=> [[G0 GU] I D A DF GA|GU]; last first.
@@ -275,7 +275,7 @@ elim/Pchoice: I => I in D DF A GA *; rewrite -bigsetU_fset_set// big_seq.
 by elim/big_ind: _ => // i; rewrite in_fset_set// inE => /GA.
 Qed.
 
-Lemma finN0_bigcap_closedP T (G : set (set T)) :
+Lemma finN0_bigcap_closedP T (G : set_system T) :
   setI_closed G <-> finN0_bigcap_closed G.
 Proof.
 split=> [GI I D A DF [i Di] GA|GI A B GA GB]; last first.
@@ -288,7 +288,7 @@ rewrite in_fset_set// inE => -[Dj /eqP nij] GAB.
 by rewrite setICA; apply: GI => //; apply: GA.
 Qed.
 
-Lemma setD_closedP T (G : set (set T)) :
+Lemma setD_closedP T (G : set_system T) :
   setD_closed G <-> (setI_closed G /\ setSD_closed G).
 Proof.
 split=> [GDI|[GI GD]].
@@ -301,7 +301,7 @@ Qed.
 Notation sedDI_closedP := setD_closed (only parsing).
 
 Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T)
-    (F : I -> set (set T)) (J : set I) :
+    (F : I -> set_system T) (J : set I) :
   (forall n, J n -> sigma_algebra D (F n)) ->
   sigma_algebra D (\bigcap_(i in J) F i).
 Proof.
@@ -310,7 +310,7 @@ move=> mG; split=> [i Ji|A AJ i Ji|H GH i Ji]; first by have [] := mG i.
 - by have [_ _ mGiU] := mG i Ji; apply: mGiU => j; exact: GH.
 Qed.
 
-Lemma sigma_algebraP T U (C : set (set T)) :
+Lemma sigma_algebraP T U (C : set_system T) :
   (forall X, C X -> X `<=` U) ->
   sigma_algebra U C <->
   [/\ C U, setSD_closed C, ndseq_closed C & setI_closed C].
@@ -344,8 +344,8 @@ move=> C_subU; split => [[C0 CD CU]|[DT DC DU DI]]; split.
 Qed.
 
 Section generated_sigma_algebra.
-Context {T : Type} (D : set T) (G : set (set T)).
-Implicit Types (M : set (set T)).
+Context {T : Type} (D : set T) (G : set_system T).
+Implicit Type M : set_system T.
 
 Lemma smallest_sigma_algebra : sigma_algebra D <<s D, G >>.
 Proof.
@@ -377,8 +377,8 @@ End generated_sigma_algebra.
 #[global] Hint Resolve smallest_sigma_algebra : core.
 
 Section generated_setring.
-Context {T : Type} (G : set (set T)).
-Implicit Types (M : set (set T)).
+Context {T : Type} (G : set_system T).
+Implicit Type M : set_system T.
 
 Lemma smallest_setring : setring <<r G >>.
 Proof.
@@ -415,7 +415,7 @@ End generated_setring.
 #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setringD`")]
 Notation setringDI := setringD (only parsing).
 
-Lemma g_sigma_algebra_lambda_system T (G : set (set T)) (D : set T) :
+Lemma g_sigma_algebra_lambda_system T (G : set_system T) (D : set T) :
   (forall X, <<s D, G >> X -> X `<=` D) ->
   lambda_system D <<s D, G >>.
 Proof.
@@ -423,7 +423,7 @@ move=> sDGD; have := smallest_sigma_algebra D G.
 by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split.
 Qed.
 
-Lemma smallest_sigma_ring T (G : set (set T)) : sigma_ring <<sr G >>.
+Lemma smallest_sigma_ring T (G : set_system T) : sigma_ring <<sr G >>.
 Proof.
 split=> [B [[]]//|A B GA GB C [[? CDI ?]] GC|A GA C [[? ? CU]] GC] /=.
 - by apply: (CDI); [exact: GA|exact: GB].
@@ -431,21 +431,21 @@ split=> [B [[]]//|A B GA GB C [[? CDI ?]] GC|A GA C [[? ? CU]] GC] /=.
 Qed.
 
 (**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(1), p.27 *)
-Lemma sigma_ring_monotone T (G : set (set T)) : sigma_ring G -> monotone G.
+Lemma sigma_ring_monotone T (G : set_system T) : sigma_ring G -> monotone G.
 Proof.
 move=> [G0 GDI GU]; split => [F ndF GF|F icF GF]; first exact: GU.
 rewrite -(@setD_bigcup _ _ F _ O)//; apply: (GDI); first exact: GF.
 by rewrite bigcup_mkcond; apply: GU => n; case: ifPn => // _; exact: GDI.
 Qed.
 
-Lemma g_sigma_ring_monotone T (G : set (set T)) : monotone <<sr G >>.
+Lemma g_sigma_ring_monotone T (G : set_system T) : monotone <<sr G >>.
 Proof. by apply: sigma_ring_monotone => //; exact: smallest_sigma_ring. Qed.
 
-Lemma sub_g_sigma_ring T (G : set (set T)) : G `<=` <<sr G >>.
+Lemma sub_g_sigma_ring T (G : set_system T) : G `<=` <<sr G >>.
 Proof. exact: sub_smallest. Qed.
 
 (**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(2), p.27 *)
-Lemma setring_monotone_sigma_ring T (G : set (set T)) :
+Lemma setring_monotone_sigma_ring T (G : set_system T) :
   setring G -> monotone G -> sigma_ring G.
 Proof.
 move=> [G0 GU GD] [ndG niG]; split => // F GF.
@@ -454,7 +454,7 @@ rewrite -bigcup_bigsetU_bigcup; apply: ndG.
 by elim=> [|n ih]; rewrite big_ord_recr/= ?big_ord0 ?set0U//; exact: GU.
 Qed.
 
-Lemma g_monotone_monotone T (G : set (set T)) : monotone <<M G>>.
+Lemma g_monotone_monotone T (G : set_system T) : monotone <<M G>>.
 Proof.
 split=> /= F ndF GF C [[ndC niC] GC];
   have {}GC : <<M G >> `<=` C by exact: smallest_sub.
@@ -463,7 +463,7 @@ split=> /= F ndF GF C [[ndC niC] GC];
 Qed.
 
 Section g_monotone_g_sigma_ring.
-Variables (T : Type) (G : set (set T)).
+Variables (T : Type) (G : set_system T).
 Hypothesis ringG : setring G.
 
 (**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.B, p.27 *)
@@ -527,14 +527,14 @@ Qed.
 
 End g_monotone_g_sigma_ring.
 
-Corollary monotone_setring_sub_g_sigma_ring T (G R : set (set T)) : monotone G ->
+Corollary monotone_setring_sub_g_sigma_ring T (G R : set_system T) : monotone G ->
   setring R -> R `<=` G -> <<sr R>> `<=` G.
 Proof.
 by move=> mG rR RG; rewrite -g_monotone_g_sigma_ring//; exact: smallest_sub.
 Qed.
 
 Section smallest_lambda_system.
-Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T).
+Variables (T : Type) (G : set_system T) (setIG : setI_closed G) (D : set T).
 Hypothesis lambdaDG : lambda_system D <<l D, G >>.
 
 Lemma smallest_lambda_system : (forall X, <<s D, G >> X -> X `<=` D) ->
@@ -586,8 +586,8 @@ Qed.
 End smallest_lambda_system.
 
 Section lambda_system_subset.
-Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T).
-Variables (H : set (set T)) (DH : lambda_system D H) (GH : G `<=` H).
+Variables (T : Type) (G : set_system T) (setIG : setI_closed G) (D : set T).
+Variables (H : set_system T) (DH : lambda_system D H) (GH : G `<=` H).
 
 (**md a.k.a. Sierpiński–Dynkin's pi-lambda theorem *)
 Lemma lambda_system_subset : (forall X, (<<s D, G >>) X -> X `<=` D) ->
@@ -603,7 +603,7 @@ End lambda_system_subset.
 
 Section dynkin.
 Variable T : Type.
-Implicit Types G D : set (set T).
+Implicit Types G D : set_system T.
 
 Lemma dynkinT G : dynkin G -> G setT. Proof. by case. Qed.
 
@@ -616,7 +616,7 @@ End dynkin.
 
 Section dynkin_lemmas.
 Variable T : Type.
-Implicit Types D G : set (set T).
+Implicit Types D G : set_system T.
 
 Lemma dynkin_lambda_system G : dynkin G <-> lambda_system setT G.
 Proof.
@@ -728,7 +728,7 @@ End dynkin_lemmas.
 
 Section trace.
 Variable (T : Type).
-Implicit Types (G : set (set T)) (A D : set T).
+Implicit Types (G : set_system T) (A D : set T).
 
 Definition strace G D := [set x `&` D | x in G].
 
@@ -845,7 +845,7 @@ Qed.
 End trace.
 
 HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable0 : measurable set0 ;
   measurableI : setI_closed measurable;
   semi_measurableD : semi_setD_closed measurable;
@@ -904,7 +904,7 @@ HB.structure Definition SigmaRing d :=
   {T of SemiRingOfSets d T & hasMeasurableCountableUnion d T}.
 
 HB.factory Record isSigmaRing (d : measure_display) T & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable0 : measurable set0 ;
   measurableD : setD_closed measurable ;
   bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) ->
@@ -935,7 +935,7 @@ HB.structure Definition Measurable d :=
 HB.structure Definition PMeasurable d := {T of Pointed T & Measurable d T}.
 
 HB.factory Record isRingOfSets (d : measure_display) T & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
   measurableD : setD_closed measurable;
@@ -959,7 +959,7 @@ HB.end.
 
 HB.factory Record isRingOfSets_setY (d : measure_display) T
     & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable_nonempty : measurable !=set0 ;
   measurable_setY : setY_closed measurable ;
   measurable_setI : setI_closed measurable }.
@@ -990,7 +990,7 @@ HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD.
 HB.end.
 
 HB.factory Record isAlgebraOfSets (d : measure_display) T & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
   measurableC : setC_closed measurable
@@ -1015,7 +1015,7 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 HB.end.
 
 HB.factory Record isAlgebraOfSets_setD (d : measure_display) T & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurableT : measurable [set: T] ;
   measurableD : setD_closed measurable
 }.
@@ -1039,7 +1039,7 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 HB.end.
 
 HB.factory Record isMeasurable (d : measure_display) T & Choice T := {
-  measurable : set (set T) ;
+  measurable : set_system T ;
   measurable0 : measurable set0 ;
   measurableC : forall A, measurable A -> measurable (~` A) ;
   measurable_bigcup : forall F : (set T)^nat, (forall i, measurable (F i)) ->
@@ -1160,7 +1160,7 @@ Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed.
 End sigmaring_lemmas.
 
 (* Adapted from mathlib induction_on_inter *)
-Lemma dynkin_induction d {T : measurableType d} (G : set (set T))
+Lemma dynkin_induction d {T : measurableType d} (G : set_system T)
     (P : set_system T) :
   @measurable _ T = <<s G >> ->
   setI_closed G ->
@@ -1249,7 +1249,7 @@ End measurable_lemmas.
 Section discrete_measurable.
 Context {T : Type}.
 
-Definition discrete_measurable : set (set T) := [set: set T].
+Definition discrete_measurable : set_system T := [set: set T].
 
 Lemma discrete_measurable0 : discrete_measurable set0. Proof. by []. Qed.
 
@@ -1276,13 +1276,13 @@ HB.instance Definition _ := @isMeasurable.Build default_measure_display
   nat discrete_measurable discrete_measurable0
   discrete_measurableC discrete_measurableU.
 
-Definition sigma_display {T} : set (set T) -> measure_display.
+Definition sigma_display {T} : set_system T -> measure_display.
 Proof. exact. Qed.
 
-Definition g_sigma_algebraType {T} (G : set (set T)) := T.
+Definition g_sigma_algebraType {T} (G : set_system T) := T.
 
 Section g_salgebra_instance.
-Variables (T : choiceType) (G : set (set T)).
+Variables (T : choiceType) (G : set_system T).
 
 Lemma sigma_algebraC (A : set T) : <<s G >> A -> <<s G >> (~` A).
 Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed.
@@ -1297,15 +1297,15 @@ End g_salgebra_instance.
 
 Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
 Notation "G .-sigma.-measurable" :=
-  (measurable : set (set (g_sigma_algebraType G))) : classical_set_scope.
+  (measurable : set_system (g_sigma_algebraType G)) : classical_set_scope.
 
-Lemma measurable_g_measurableTypeE (T : choiceType) (G : set (set T)) :
+Lemma measurable_g_measurableTypeE (T : choiceType) (G : set_system T) :
   sigma_algebra setT G -> G.-sigma.-measurable = G.
 Proof. exact: sigma_algebra_id. Qed.
 
 Section measurability.
 
-Lemma sigma_algebra_preimage (aT rT : Type) (G : set (set rT))
+Lemma sigma_algebra_preimage (aT rT : Type) (G : set_system rT)
     (D : set aT) (f : aT -> rT) :
   sigma_algebra setT G -> sigma_algebra D (preimage_set_system D f G).
 Proof.
@@ -1373,10 +1373,10 @@ End preimage_generated_sigma_algebra.
 
 Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
 Notation "f .-preimage.-measurable" :=
-  (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
+  (measurable : set_system (g_sigma_algebra_preimageType f)) : classical_set_scope.
 
 Lemma sigma_algebra_image (aT rT : Type) (D : set aT) (f : aT -> rT)
-    (G : set (set aT)) :
+    (G : set_system aT) :
   sigma_algebra D G -> sigma_algebra setT (image_set_system D f G).
 Proof.
 move=> [G0 GC GU]; split; rewrite /image_set_system.
@@ -1390,7 +1390,7 @@ move=> [G0 GC GU]; split; rewrite /image_set_system.
 Qed.
 
 Lemma g_sigma_preimageE aT (rT : choiceType) (D : set aT)
-    (f : aT -> rT) (G' : set (set rT)) :
+    (f : aT -> rT) (G' : set_system rT) :
   <<s D, preimage_set_system D f G' >> =
     preimage_set_system D f (G'.-sigma.-measurable).
 Proof.
@@ -1404,7 +1404,7 @@ rewrite eqEsubset; split.
   exact: smallest_sub.
 have G'pre A' : G' A' -> (preimage_set_system D f G') (D `&` f @^-1` A').
   by move=> ?; exists A'.
-pose I : set (set aT) := <<s D, preimage_set_system D f G' >>.
+pose I : set_system aT := <<s D, preimage_set_system D f G' >>.
 have G'sfun : G' `<=` image_set_system D f I.
   by move=> A' /G'pre[B G'B h]; apply: sub_sigma_algebra; exists B.
 have sG'sfun : <<s G' >> `<=` image_set_system D f I.
@@ -1443,7 +1443,7 @@ Qed.
 
 Section covering.
 Context {T : Type}.
-Implicit Type (C : forall I, set (set I)).
+Implicit Type (C : forall I, set_system I).
 Implicit Type (P : forall I, set I -> set (I -> set T)).
 
 (* TODO: undocumented *)
@@ -1584,7 +1584,8 @@ Let prod_salgebra_bigcup (F : _^nat) :
   g_sigma_preimageU f1 f2 (\bigcup_i (F i)).
 Proof. exact: sigma_algebra_bigcup. Qed.
 
-HB.instance Definition _ := Choice.on (T1 * T2)%type.
+(*HB.instance Definition _ := Choice.on (T1 * T2)%type.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 HB.instance Definition prod_salgebra_mixin :=
   @isMeasurable.Build (measure_prod_display (d1, d2))
     (T1 * T2)%type (g_sigma_preimageU f1 f2)
@@ -1593,7 +1594,7 @@ HB.instance Definition prod_salgebra_mixin :=
 End product_salgebra_instance.
 Notation "p .-prod" := (measure_prod_display p) : measure_display_scope.
 Notation "p .-prod.-measurable" :=
-  ((p.-prod).-measurable : set (set (_ * _))) :
+  ((p.-prod).-measurable : set_system (_ * _)) :
     classical_set_scope.
 
 Lemma measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2)
@@ -1637,7 +1638,7 @@ End product_salgebra_algebraOfSetsType.
 Notation measurable_prod_measurableType := prod_measurable_rectangle (only parsing).
 
 Section product_salgebra_g_measurableTypeR.
-Context d1 (T1 : algebraOfSetsType d1) (T2 : choiceType) (C2 : set (set T2)).
+Context d1 (T1 : algebraOfSetsType d1) (T2 : choiceType) (C2 : set_system T2).
 Hypothesis setTC2 : setT `<=` C2.
 
 #[deprecated(since="mathcomp-analysis 1.17.0")]
@@ -1654,7 +1655,7 @@ Qed.
 End product_salgebra_g_measurableTypeR.
 
 Section product_salgebra_g_measurableType.
-Variables (T1 T2 : choiceType) (C1 : set (set T1)) (C2 : set (set T2)).
+Variables (T1 T2 : choiceType) (C1 : set_system T1) (C2 : set_system T2).
 Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).
 
 #[deprecated(since="mathcomp-analysis 1.17.0")]
@@ -1671,7 +1672,7 @@ Qed.
 End product_salgebra_g_measurableType.
 
 Definition g_sigma_preimage d (rT : semiRingOfSetsType d) (aT : Type)
-    (n : nat) (f : 'I_n -> aT -> rT) : set (set aT) :=
+    (n : nat) (f : 'I_n -> aT -> rT) : set_system aT :=
   <<s \big[setU/set0]_(i < n) preimage_set_system setT (f i) measurable >>.
 
 Lemma g_sigma_preimage_comp d1 {T1 : semiRingOfSetsType d1} n
diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v
index 79f541ce6..370111726 100644
--- a/theories/measure_theory/measure_extension.v
+++ b/theories/measure_theory/measure_extension.v
@@ -399,7 +399,7 @@ Definition caratheodory_type (R : realType) (T : Type)
   (mu : set T -> \bar R) := T.
 
 Notation "mu .-cara.-measurable" :=
-  (measurable : set (set (caratheodory_type mu))) : classical_set_scope.
+  (measurable : set_system (caratheodory_type mu)) : classical_set_scope.
 
 Definition caratheodory_display R T : (set T -> \bar R) -> measure_display.
 Proof. exact. Qed.
diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index 2d997d928..32e3fdb20 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -709,10 +709,10 @@ HB.instance Definition _ := isRingOfSets.Build (display d) rT
 
 Local Notation "d .-ring" := (display d).
 Local Notation "d .-ring.-measurable" :=
-  ((d%mdisp.-ring).-measurable : set (set (type _))).
+  ((d%mdisp.-ring).-measurable : set_system (type _)).
 
-Local Definition measurable_fin_trivIset : set (set T) :=
-  [set A | exists B : set (set T),
+Local Definition measurable_fin_trivIset : set_system T :=
+  [set A | exists B : set_system T,
     [/\ A = \bigcup_(X in B) X, forall X : set T, B X -> measurable X,
       finite_set B & trivIset B id]].
 
@@ -769,10 +769,10 @@ rewrite -bigcup2inE; apply: mdU => //; last by move=> [|[]]// _; apply: mdDI.
 by move=> [|[]]// [|[]]//= _ _ []; rewrite setDE ?setIA => X [] []//.
 Qed.
 
-Lemma measurable_subring : (d.-measurable : set (set T)) `<=` d.-ring.-measurable.
+Lemma measurable_subring : (d.-measurable : set_system T) `<=` d.-ring.-measurable.
 Proof. by rewrite /measurable => X Xmeas /= M /= [_]; apply. Qed.
 
-Lemma ring_finite_set (A : set rT) : measurable A -> exists B : set (set T),
+Lemma ring_finite_set (A : set rT) : measurable A -> exists B : set_system T,
   [/\ finite_set B,
       (forall X, B X -> X !=set0),
       trivIset B id,
@@ -789,7 +789,7 @@ rewrite bigcup_mkcondr; apply: eq_bigcupr => X Bx; case: ifPn => //.
 by rewrite notin_setE/= => /negP/negPn/eqP.
 Qed.
 
-Definition decomp (A : set rT) : set (set T) :=
+Definition decomp (A : set rT) : set_system T :=
   if A == set0 then [set set0] else
   if pselect (measurable A) is left mA then projT1 (cid (ring_finite_set mA))
   else [set A].
@@ -930,7 +930,7 @@ End SetRing.
 Export SetRing.Exports.
 Notation "d .-ring" := (SetRing.display d) : measure_display_scope.
 Notation "d .-ring.-measurable" :=
-  ((d%mdisp.-ring).-measurable : set (set (SetRing.type _))) : classical_set_scope.
+  ((d%mdisp.-ring).-measurable : set_system (SetRing.type _)) : classical_set_scope.
 
 Lemma le_measure d (R : realFieldType) (T : semiRingOfSetsType d)
     (mu : {content set T -> \bar R}) :
@@ -1727,7 +1727,7 @@ End measure_continuity.
 
 Section g_sigma_algebra_measure_unique_trace.
 Context d (R : realType) (T : measurableType d).
-Variables (G : set (set T)) (D : set T) (mD : measurable D).
+Variables (G : set_system T) (D : set T) (mD : measurable D).
 Let H := [set X | G X /\ X `<=` D] (* "trace" of G wrt D *).
 Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H).
 Variables m1 m2 : {measure set T -> \bar R}.
@@ -1869,7 +1869,7 @@ Notation le_mu_bigcup := generalized_Boole_inequality.
 
 Section g_sigma_algebra_measure_unique.
 Context d (R : realType) (T : measurableType d).
-Variable G : set (set T).
+Variable G : set_system T.
 Hypothesis Gm : G `<=` measurable.
 Variable g : (set T)^nat.
 Hypotheses Gg : forall i, G (g i).
@@ -1973,7 +1973,7 @@ Qed.
 
 Section measure_unique.
 Context d (R : realType) (T : measurableType d).
-Variables  (G : set (set T)) (g : (set T)^nat).
+Variables  (G : set_system T) (g : (set T)^nat).
 Hypotheses (mG : measurable = <<s G >>) (setIG : setI_closed G).
 Hypothesis Gg : forall i, G (g i).
 Hypothesis g_cover : \bigcup_k (g k) = setT.
diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v
index 4d32eff27..654deb43e 100644
--- a/theories/measure_theory/probability_measure.v
+++ b/theories/measure_theory/probability_measure.v
@@ -211,7 +211,7 @@ move=> mU r1; apply/seteqP; split => // x/= _.
 by rewrite /mset/= (le_lt_trans (probability_le1 _ _)).
 Qed.
 
-Definition pset : set (set (probability T R)) :=
+Definition pset : set_system (probability T R) :=
   [set mset U r | r in `[0%R,1%R] & U in measurable].
 
 Definition pprobability : measurableType pset.-sigma :=
diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v
index fda82619e..59e9d3ffb 100644
--- a/theories/normedtype_theory/ereal_normedtype.v
+++ b/theories/normedtype_theory/ereal_normedtype.v
@@ -1,4 +1,4 @@
-(* 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_compat ssralg ssrnum interval.
 From mathcomp Require Import interval_inference.
@@ -16,7 +16,7 @@ From mathcomp Require Import real_interval num_normedtype.
 (* ```                                                                        *)
 (*   limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F    *)
 (*                                   f has type X -> \bar R.                  *)
-(*                                   F has type set (set X).                  *)
+(*                                   F has type set_system X.                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Lower semicontinuous                                                    *)
@@ -42,7 +42,7 @@ Local Open Scope ring_scope.
 
 Section limf_esup_einf.
 Variables (T : choiceType) (X : filteredType T) (R : realFieldType).
-Implicit Types (f : X -> \bar R) (F : set (set X)).
+Implicit Types (f : X -> \bar R) (F : set_system X).
 Local Open Scope ereal_scope.
 
 Definition limf_esup f F := ereal_inf [set ereal_sup (f @` V) | V in F].
@@ -71,7 +71,7 @@ End limf_esup_einf.
 
 Section limf_esup_einf_realType.
 Variables (T : choiceType) (X : filteredType T) (R : realType).
-Implicit Types (f : X -> \bar R) (F : set (set X)).
+Implicit Types (f : X -> \bar R) (F : set_system X).
 Local Open Scope ereal_scope.
 
 Lemma limf_esup_ge0 f F : ~ F set0 ->
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index c57a771ab..1252178b3 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -221,8 +221,9 @@ HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := NormedModule.copy R R^o.
-#[export, non_forgetful_inheritance]
-HB.instance Definition _ := Num.RealField.on R.
+(*#[export, non_forgetful_inheritance]
+HB.instance Definition _ := Num.RealField.on R.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 End realFieldType.
 
 Section numClosedFieldType.
@@ -245,8 +246,9 @@ HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := NormedModule.copy R R^o.
-#[export, non_forgetful_inheritance]
-HB.instance Definition _ := Num.NumField.on R.
+(*#[export, non_forgetful_inheritance]
+HB.instance Definition _ := Num.NumField.on R.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 End numFieldType.
 
 Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports.
@@ -1559,7 +1561,7 @@ Qed.
 Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R.
 Proof. by rewrite /Rhull -set_itvNyy asboolF// asboolF. Qed.
 
-Lemma RhullK : {in (@is_interval _ : set (set R)), cancel Rhull pred_set}.
+Lemma RhullK : {in (@is_interval _ : set_system R), cancel Rhull pred_set}.
 Proof. by move=> X /asboolP iX; exact/esym/is_intervalP. Qed.
 
 Lemma set_itv_setT (i : interval R) : [set` i] = setT -> i = `]-oo, +oo[.
diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v
index 6ec498270..737854829 100644
--- a/theories/normedtype_theory/urysohn.v
+++ b/theories/normedtype_theory/urysohn.v
@@ -746,7 +746,8 @@ Definition type : Type := let _ := completely_regular_nbhsE in X.
   (@entourage_inv X')
   (@entourage_split_ex X')
   completely_regular_nbhsE.
-#[export] HB.instance Definition _ := Uniform.on type.
+(*#[export] HB.instance Definition _ := Uniform.on type.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 End completely_regular_uniformity.
 Module Exports. HB.reexport. End Exports.
diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v
index 4d6ec3844..bc2974b21 100644
--- a/theories/probability_theory/bernoulli_distribution.v
+++ b/theories/probability_theory/bernoulli_distribution.v
@@ -188,7 +188,7 @@ Implicit Type p : R.
 Lemma measurable_bernoulli_prob :
   measurable_fun setT (bernoulli_prob : R -> pprobability bool R).
 Proof.
-apply: (measurability (@pset _ _ _ : set (set (pprobability _ R)))) => //.
+apply: (measurability (@pset _ _ _ : set_system (pprobability _ R))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
 apply: measurable_fun_ifT => //=.
   by apply: measurable_and => //; exact: measurable_fun_ler.
diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v
index 4b8443366..40d598cff 100644
--- a/theories/probability_theory/binomial_distribution.v
+++ b/theories/probability_theory/binomial_distribution.v
@@ -185,7 +185,7 @@ Qed.
 Lemma measurable_binomial_prob (R : realType) (n : nat) :
   measurable_fun setT (binomial_prob n : R -> pprobability _ _).
 Proof.
-apply: (measurability (@pset _ _ _ : set (set (pprobability _ R)))) => //.
+apply: (measurability (@pset _ _ _ : set_system (pprobability _ R))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
 apply: measurable_fun_if => //=.
   by apply: measurable_and => //; exact: measurable_fun_ler.
diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v
index 72215b630..f250b5295 100644
--- a/theories/probability_theory/poisson_distribution.v
+++ b/theories/probability_theory/poisson_distribution.v
@@ -112,7 +112,7 @@ End poisson.
 Lemma measurable_poisson_prob {R : realType} n :
   measurable_fun setT (poisson_prob ^~ n : R -> pprobability _ _).
 Proof.
-apply: (measurability (@pset _ _ _ : set (set (pprobability _ R)))) => //.
+apply: (measurability (@pset _ _ _ : set_system (pprobability _ R))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
 apply: measurable_fun_if => //=; first exact: measurable_fun_ltr.
 apply: (eq_measurable_fun (fun t =>
diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v
index 3476d4b56..7b0b1167e 100644
--- a/theories/topology_theory/discrete_topology.v
+++ b/theories/topology_theory/discrete_topology.v
@@ -40,7 +40,7 @@ HB.mixin Record Discrete_ofNbhs T & Nbhs T := {
 #[short(type="discreteNbhsType")]
 HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}.
 
-Definition discrete_ent {T} : set (set (T * T)) :=
+Definition discrete_ent {T} : set_system (T * T) :=
   globally (range (fun x => (x, x))).
 
 (** Note: having the discrete topology does not guarantee the discrete
diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index 40dbfdc30..8c82e106d 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -567,10 +567,11 @@ HB.instance Definition _ (U : topologicalType) (T : uniformType) :=
     (continuousType U T)
     (initial_topology (id : continuousType U T -> (U -> T))).
 
-HB.instance Definition _ (U : topologicalType) (R : realType)
+(*HB.instance Definition _ (U : topologicalType) (R : realType)
      (T : pseudoMetricType R) :=
   PseudoMetric.on
-    (initial_topology (id : continuousType U T -> (U -> T))).
+    (initial_topology (id : continuousType U T -> (U -> T))).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 End ArrowAsUniformType.
 
diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v
index 545a8fc5c..5e6a91d83 100644
--- a/theories/topology_theory/matrix_topology.v
+++ b/theories/topology_theory/matrix_topology.v
@@ -145,16 +145,21 @@ by apply: filter_bigI => ??; apply: entP.
 Unshelve. all: by end_near. Qed.
 
 Section matrix_PointedTopology.
-Variables (m n : nat) .
+Variables (m n : nat).
 HB.instance Definition _ (T : ptopologicalType) := Filtered.on 'M[T]_(m, n).
-HB.instance Definition _ (T : ptopologicalType) := Pointed.on 'M[T]_(m, n).
-HB.instance Definition _ (T : ptopologicalType) :=
-  PointedFiltered.on 'M[T]_(m, n).
-HB.instance Definition _ (T : ptopologicalType) :=
-  PointedTopological.on 'M[T]_(m, n).
-HB.instance Definition _ (T : uniformType) := Uniform.on 'M[T]_(m, n).
+(*HB.instance Definition _ (T : ptopologicalType) := Pointed.on 'M[T]_(m, n).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
+(*HB.instance Definition _ (T : ptopologicalType) :=
+  PointedFiltered.on 'M[T]_(m, n).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
+(*HB.instance Definition _ (T : ptopologicalType) :=
+  PointedTopological.on 'M[T]_(m, n).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
+(*HB.instance Definition _ (T : uniformType) := Uniform.on 'M[T]_(m, n).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 HB.instance Definition _ (T : puniformType) := Pointed.on 'M[T]_(m, n).
-HB.instance Definition _ (T : puniformType) := PointedUniform.on 'M[T]_(m, n).
+(*HB.instance Definition _ (T : puniformType) := PointedUniform.on 'M[T]_(m, n).*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 End matrix_PointedTopology.
 
 Section matrix_Complete.
diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index da7844913..72c415b3b 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -45,7 +45,8 @@ move=> [QR [/nbhs_interior p1_Q /nbhs_interior p2_R] sQRA].
 by exists (QR.1°, QR.2°) => // ??; exists QR.
 Qed.
 
-HB.instance Definition _ := hasNbhs.Build (T * U)%type prod_nbhs.
+(*HB.instance Definition _ := hasNbhs.Build (T * U)%type prod_nbhs.*)
+(* generates: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 HB.instance Definition _ := Nbhs_isNbhsTopological.Build (T * U)%type
   prod_nbhs_filter prod_nbhs_singleton prod_nbhs_nbhs.
diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index 3071877d5..ef6d7a6e3 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -707,8 +707,9 @@ move=> x; apply: continuous_comp; last exact: continuous_fun.
 exact/subspaceT_continuous/continuous_fun.
 Qed.
 
-HB.instance Definition _ :=
-  @isContinuous.Build (subspace A) Z (g \o f) continuous_comp_subproof.
+(*HB.instance Definition _ :=
+  @isContinuous.Build (subspace A) Z (g \o f) continuous_comp_subproof.*)
+(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
 
 End continuous_fun_comp.
 
diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v
index 72d89a081..c4a963df4 100644
--- a/theories/topology_theory/supremum_topology.v
+++ b/theories/topology_theory/supremum_topology.v
@@ -179,7 +179,7 @@ Lemma countable_sup_ent :
   countable_uniformity Tt.
 Proof.
 move=> Icnt countable_ent; pose f n := cid (countable_ent n).
-pose g (n : Ii) : set (set (T * T)) := projT1 (f n).
+pose g (n : Ii) : set_system (T * T) := projT1 (f n).
 have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0.
   exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|].
   move=> P [w [A _]] <- subP; exists setT => //.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index 666115914..a6170e44b 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -122,7 +122,7 @@ Context {T : topologicalType}.
 
 Definition open_nbhs (p : T) (A : set T) := open A /\ A p.
 
-Definition basis (B : set (set T)) :=
+Definition basis (B : set_system T) :=
   B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x.
 
 Definition second_countable := exists2 B, countable B & basis B.
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 44e5ce874..f8ec6cb9a 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -166,7 +166,7 @@ End NbhsEntourage.
 Lemma nbhsP {M : uniformType} (x : M) P : nbhs x P <-> nbhs_ entourage x P.
 Proof. by rewrite nbhs_simpl. Qed.
 
-Lemma filter_inv {T : Type} (F : set (set (T * T))) :
+Lemma filter_inv {T : Type} (F : set_system (T * T)) :
   Filter F -> Filter [set V^-1 | V in F]%relation.
 Proof.
 move=> FF; split => /=.