Adapt to https://github.com/rocq-prover/rocq/pull/21611

classical/classical_sets.v

@@ -2482,7 +2482,7 @@ Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.
 
 End PointedTheory.
 
-HB.mixin Record isBiPointed (X : Type) of Equality X := {
+HB.mixin Record isBiPointed (X : Type) & Equality X := {
   zero : X;
   one : X;
   zero_one_neq : zero != one;
@@ -2511,10 +2511,10 @@ HB.mixin Record isEmpty T := {
 #[short(type="emptyType")]
 HB.structure Definition Empty := {T of isEmpty T & Finite T}.
 
-HB.factory Record Choice_isEmpty T of Choice T := {
+HB.factory Record Choice_isEmpty T & Choice T := {
   axiom : T -> False
 }.
-HB.builders Context T of Choice_isEmpty T.
+HB.builders Context T & Choice_isEmpty T.
 
 Definition pickle : T -> nat := fun=> 0%N.
 Definition unpickle : nat -> option T := fun=> None.
@@ -2532,12 +2532,12 @@ HB.end.
 HB.factory Record Type_isEmpty T := {
   axiom : T -> False
 }.
-HB.builders Context T of Type_isEmpty T.
+HB.builders Context T & Type_isEmpty T.
 Definition eq_op (x y : T) := true.
 Lemma eq_opP : Equality.axiom eq_op. Proof. by move=> ? /[dup]/axiom. Qed.
 HB.instance Definition _ := hasDecEq.Build T eq_opP.
 
-Definition find of pred T & nat : option T := None.
+Definition find & pred T & nat : option T := None.
 Lemma findP (P : pred T) (n : nat) (x : T) :  find P n = Some x -> P x.
 Proof. by []. Qed.
 Lemma ex_find (P : pred T) : (exists x : T, P x) -> exists n : nat, find P n.

classical/filter.v

@@ -236,7 +236,7 @@ HB.instance Definition _ T := isFiltered.Build T (set_system T) id.
 HB.mixin Record selfFiltered T := {}.
 
 HB.factory Record hasNbhs T := { nbhs : T -> set_system T }.
-HB.builders Context T of hasNbhs T.
+HB.builders Context T & hasNbhs T.
   HB.instance Definition _ := isFiltered.Build T T nbhs.
   HB.instance Definition _ := selfFiltered.Build T.
 HB.end.
@@ -274,7 +274,7 @@ Definition prop_near1 {X} {fX : filteredType X} (x : fX)
    P (phP : ph {all1 P}) := nbhs x P.
 
 Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'}
-  (x : fX) (x' : fX') := fun P of ph {all2 P} =>
+  (x : fX) (x' : fX') := fun P & ph {all2 P} =>
   filter_prod (nbhs x) (nbhs x') (fun x => P x.1 x.2).
 
 End Near.

classical/set_interval.v

@@ -609,7 +609,7 @@ Proof. by apply/funext => x; rewrite /factor subrr invr0 mulr0. Qed.
 Lemma factorl a b : factor a b a = 0.
 Proof. by rewrite /factor subrr mul0r. Qed.
 
-Definition ndline_path a b of a < b := line_path a b.
+Definition ndline_path a b & a < b := line_path a b.
 
 Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b.
 Proof. by []. Qed.

experimental_reals/distr.v

@@ -49,7 +49,7 @@ Structure distr := Distr {
   _  :  psum mu <= 1
 }.
 
-Definition distr_of of phant R & phant T := distr.
+Definition distr_of & phant R & phant T := distr.
 End Distribution.
 
 Notation "{ 'distr' T / R }" := (distr_of (Phant R) (Phant T))

reals/constructive_ereal.v

@@ -3859,10 +3859,10 @@ Arguments cmp0e {R i} _ {_}.
 Arguments neqe0 {R i} _ {_}.
 Arguments ext_widen_itv {R i} _ {_ _}.
 
-Definition posnume (R : numDomainType) of phant R :=
+Definition posnume (R : numDomainType) & phant R :=
   Itv.def (@ext_num_sem R) (Itv.Real `]0%Z, +oo[).
 Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
-Definition nonnege (R : numDomainType) of phant R :=
+Definition nonnege (R : numDomainType) & phant R :=
   Itv.def (@ext_num_sem R) (Itv.Real `[0%Z, +oo[).
 Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
 Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)

reals/reals.v

@@ -118,7 +118,7 @@ End has_bound_lemmas.
 
 (* -------------------------------------------------------------------- *)
 
-HB.mixin Record ArchimedeanField_isReal R of Num.ArchiRealField R := {
+HB.mixin Record ArchimedeanField_isReal R & Num.ArchiRealField R := {
   sup_upper_bound_subdef : forall E : set R,
     has_sup E -> ubound E (supremum 0 E) ;
   sup_adherent_subdef : forall (E : set R) (eps : R),

reals/signed.v

@@ -320,10 +320,10 @@ Notation "x %:sgn" := (from (Phantom _ x)) : ring_scope.
 Notation "[ 'sgn' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope.
 Notation num := r.
 Notation "x %:num" := (r x) : ring_scope.
-Definition posnum (R : numDomainType) of phant R := {> 0%R : R}.
+Definition posnum (R : numDomainType) & phant R := {> 0%R : R}.
 Notation "{ 'posnum' R }" := (@posnum _ (Phant R))  : ring_scope.
 Notation "x %:posnum" := (@num _ _ 0%R !=0 >=0 x) : ring_scope.
-Definition nonneg (R : numDomainType) of phant R := {>= 0%R : R}.
+Definition nonneg (R : numDomainType) & phant R := {>= 0%R : R}.
 Notation "{ 'nonneg' R }" := (@nonneg _ (Phant R))  : ring_scope.
 Notation "x %:nngnum" := (@num _ _ 0%R ?=0 >=0 x) : ring_scope.
 Arguments r {disp T x0 nz cond}.

theories/charge.v

@@ -133,7 +133,7 @@ HB.factory Record isCharge d (T : semiRingOfSetsType d) (R : realFieldType)
 }.
 
 HB.builders Context d (T : semiRingOfSetsType d) (R : realFieldType)
-  mu of isCharge d T R mu.
+  mu & isCharge d T R mu.
 
 Let finite : fin_num_fun mu. Proof. exact: charge_finite. Qed.
 
@@ -224,7 +224,7 @@ End charge_lemmas.
 #[export] Hint Resolve charge_semi_additive2 : core.
 
 Definition measure_of_charge d (T : semiRingOfSetsType d) (R : numFieldType)
-  (nu : set T -> \bar R) of (forall E, 0 <= nu E) := nu.
+  (nu : set T -> \bar R) & (forall E, 0 <= nu E) := nu.
 
 Section measure_of_charge.
 Context d (T : ringOfSetsType d) (R : realFieldType).
@@ -283,7 +283,7 @@ Qed.
 End charge_lemmas_realFieldType.
 
 Definition crestr d (T : semiRingOfSetsType d) (R : numDomainType) (D : set T)
-  (f : set T -> \bar R) of measurable D := fun X => f (X `&` D).
+  (f : set T -> \bar R) & measurable D := fun X => f (X `&` D).
 
 Section charge_restriction.
 Context d (T : measurableType d) (R : numFieldType).
@@ -556,7 +556,7 @@ HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu f)
 End pushforward_charge.
 
 HB.builders Context d (T : measurableType d) (R : realType)
-  (mu : set T -> \bar R) of Measure_isFinite d T R mu.
+  (mu : set T -> \bar R) & Measure_isFinite d T R mu.
 
 Let mu0 : mu set0 = 0.
 Proof. by apply: measure0. Qed.

theories/hoelder.v

@@ -787,7 +787,7 @@ Definition finite_norm d (T : measurableType d) (R : realType)
 
 HB.mixin Record isLfunction d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R)
-  of @MeasurableFun d _ T R f := {
+  & @MeasurableFun d _ T R f := {
   Lfunction_finite : finite_norm mu p f
 }.
 

theories/homotopy_theory/continuous_path.v

@@ -40,7 +40,7 @@ Local Open Scope ring_scope.
 Local Open Scope quotient_scope.
 
 HB.mixin Record isPath {i : bpTopologicalType} {T : topologicalType} (x y : T)
-    (f : i -> T) of isContinuous i T f := {
+    (f : i -> T) & isContinuous i T f := {
   path_zero : f zero = x;
   path_one : f one = y;
 }.

theories/kernel.v

@@ -319,11 +319,11 @@ Arguments measure_uub {_ _ _ _ _} _.
 
 HB.factory Record Kernel_isFinite d d'
     (X : measurableType d) (Y : measurableType d') (R : realType)
-    (k : X -> {measure set Y -> \bar R}) of isKernel _ _ _ _ _ k := {
+    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ _ _ _ k := {
   measure_uub : measure_fam_uub k }.
 
 HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
-  (R : realType) k of Kernel_isFinite d d' X Y R k.
+  (R : realType) k & Kernel_isFinite d d' X Y R k.
 
 Let sfinite_finite :
   exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) &
@@ -411,12 +411,12 @@ HB.instance Definition _
 
 HB.factory Record Kernel_isSFinite d d'
     (X : measurableType d) (Y : measurableType d') (R : realType)
-    (k : X -> {measure set Y -> \bar R}) of isKernel _ _ _ _ _ k := {
+    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ _ _ _ k := {
   sfinite : exists s : (R.-fker X ~> Y)^nat,
     forall x U, measurable U -> k x U = kseries s x U }.
 
 HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
-  (R : realType) k of Kernel_isSFinite d d' X Y R k.
+  (R : realType) k & Kernel_isSFinite d d' X Y R k.
 
 Lemma sfinite_subdef : isSFiniteKernel_subdef d d' X Y R k.
 Proof.
@@ -500,11 +500,11 @@ Proof. by apply: (sprob_kernelP (fun x A => k x A)).1; exact: sprob_kernel. Qed.
 
 HB.factory Record Kernel_isSubProbability d d'
     (X : measurableType d) (Y : measurableType d') (R : realType)
-    (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := {
+    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ X Y R k := {
   sprob_kernel : ereal_sup [set k x [set: Y] | x in [set: X]] <= 1 }.
 
 HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
-  (R : realType) k of Kernel_isSubProbability d d' X Y R k.
+  (R : realType) k & Kernel_isSubProbability d d' X Y R k.
 
 Let finite : @Kernel_isFinite d d' X Y R k.
 Proof.
@@ -545,11 +545,11 @@ Notation "R .-pker X ~> Y" := (probability_kernel X%type Y R).
 
 HB.factory Record Kernel_isProbability d d'
     (X : measurableType d) (Y : measurableType d') (R : realType)
-    (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := {
+    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ X Y R k := {
   prob_kernel : forall x, k x [set: Y] = 1 }.
 
 HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
-  (R : realType) k of Kernel_isProbability d d' X Y R k.
+  (R : realType) k & Kernel_isProbability d d' X Y R k.
 
 Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k.
 Proof.

theories/landau.v

@@ -319,7 +319,7 @@ Proof. by case: f => ?. Qed.
 Hint Resolve littleo_class : core.
 
 Definition littleo_clone (F : set_system T) (g : T -> W) (f : T -> V) (fT : {o_F g}) c
-  of phant_id (littleo_class fT) c := @Littleo F g f c.
+  & phant_id (littleo_class fT) c := @Littleo F g f c.
 Notation "[littleo 'of' f 'for' fT ]" := (@littleo_clone _ _ f fT _ idfun).
 Notation "[littleo 'of' f ]" := (@littleo_clone _ _ f _ _ idfun).
 
@@ -505,7 +505,7 @@ Proof. by case: f => ?. Qed.
 Hint Resolve bigO_class : core.
 
 Definition bigO_clone (F : set_system T) (g : T -> W) (f : T -> V) (fT : {O_F g}) c
-  of phant_id (bigO_class fT) c := @BigO F g f c.
+  & phant_id (bigO_class fT) c := @BigO F g f c.
 Notation "[bigO 'of' f 'for' fT ]" := (@bigO_clone _ _ f fT _ idfun).
 Notation "[bigO 'of' f ]" := (@bigO_clone _ _ f _ _ idfun).
 
@@ -1232,7 +1232,7 @@ Proof. by case: f => ?. Qed.
 Hint Resolve bigOmega_class : core.
 
 Definition bigOmega_clone {W} (F : set_system T) (g : T -> W) (f : T -> V)
-  (fT : {Omega_F g}) c of phant_id (bigOmega_class fT) c := @BigOmega W F g f c.
+  (fT : {Omega_F g}) c & phant_id (bigOmega_class fT) c := @BigOmega W F g f c.
 Notation "[bigOmega 'of' f 'for' fT ]" := (@bigOmega_clone _ _ _ f fT _ idfun).
 Notation "[bigOmega 'of' f ]" := (@bigOmega_clone _ _ _ f _ _ idfun).
 
@@ -1372,7 +1372,7 @@ Proof. by case: f => ?. Qed.
 Hint Resolve bigTheta_class : core.
 
 Definition bigTheta_clone {W} (F : set_system T) (g : T -> W) (f : T -> V)
-  (fT : {Theta_F g}) c of phant_id (bigTheta_class fT) c := @BigTheta W F g f c.
+  (fT : {Theta_F g}) c & phant_id (bigTheta_class fT) c := @BigTheta W F g f c.
 Notation "[bigTheta 'of' f 'for' fT ]" := (@bigTheta_clone _ _ _ f fT _ idfun).
 Notation "[bigTheta 'of' f ]" := (@bigTheta_clone _ _ _ f _ _ idfun).
 

theories/measurable_realfun.v

@@ -1160,7 +1160,7 @@ HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f).
 HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g).
 HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g).
 
-Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D.
+Definition mindic (D : set aT) & measurable D : aT -> rT := \1_D.
 
 Lemma mindicE (D : set aT) (mD : measurable D) :
   mindic mD = (fun x => (x \in D)%:R).

theories/measure_theory/measurable_structure.v

@@ -866,28 +866,28 @@ Notation "d .-measurable" := (@measurable d%mdisp) : classical_set_scope.
 Notation "'measurable" :=
   (@measurable default_measure_display) : classical_set_scope.
 
-HB.mixin Record SemiRingOfSets_isRingOfSets d T of SemiRingOfSets d T := {
+HB.mixin Record SemiRingOfSets_isRingOfSets d T & SemiRingOfSets d T := {
   measurableU : @setU_closed T measurable
 }.
 
 #[short(type="ringOfSetsType")]
 HB.structure Definition RingOfSets d :=
   {T of SemiRingOfSets d T & SemiRingOfSets_isRingOfSets d T }.
 
-HB.mixin Record RingOfSets_isAlgebraOfSets d T of RingOfSets d T := {
+HB.mixin Record RingOfSets_isAlgebraOfSets d T & RingOfSets d T := {
   measurableT : measurable [set: T]
 }.
 
 #[short(type="algebraOfSetsType")]
 HB.structure Definition AlgebraOfSets d :=
   {T of RingOfSets d T & RingOfSets_isAlgebraOfSets d T }.
 
-HB.mixin Record hasMeasurableCountableUnion d T of SemiRingOfSets d T := {
+HB.mixin Record hasMeasurableCountableUnion d T & SemiRingOfSets d T := {
   bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) ->
     measurable (\bigcup_i (F i))
 }.
 
-HB.builders Context d T of hasMeasurableCountableUnion d T.
+HB.builders Context d T & hasMeasurableCountableUnion d T.
 
 Let mU : @setU_closed T measurable.
 Proof.
@@ -903,15 +903,15 @@ HB.end.
 HB.structure Definition SigmaRing d :=
   {T of SemiRingOfSets d T & hasMeasurableCountableUnion d T}.
 
-HB.factory Record isSigmaRing (d : measure_display) T of Pointed T := {
+HB.factory Record isSigmaRing (d : measure_display) T & Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableD : setD_closed measurable ;
   bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) ->
     measurable (\bigcup_i (F i))
 }.
 
-HB.builders Context d T of isSigmaRing d T.
+HB.builders Context d T & isSigmaRing d T.
 
 Let m0 : measurable set0. Proof. exact: measurable0. Qed.
 
@@ -931,14 +931,14 @@ HB.end.
 HB.structure Definition Measurable d :=
   {T of AlgebraOfSets d T & hasMeasurableCountableUnion d T }.
 
-HB.factory Record isRingOfSets (d : measure_display) T of Pointed T := {
+HB.factory Record isRingOfSets (d : measure_display) T & Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
   measurableD : setD_closed measurable;
 }.
 
-HB.builders Context d T of isRingOfSets d T.
+HB.builders Context d T & isRingOfSets d T.
 Implicit Types (A B C D : set T).
 
 Lemma mI : setI_closed measurable.
@@ -955,13 +955,13 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU.
 HB.end.
 
 HB.factory Record isRingOfSets_setY (d : measure_display) T
-    of Pointed T := {
+    & Pointed T := {
   measurable : set (set T) ;
   measurable_nonempty : measurable !=set0 ;
   measurable_setY : setY_closed measurable ;
   measurable_setI : setI_closed measurable }.
 
-HB.builders Context d T of isRingOfSets_setY d T.
+HB.builders Context d T & isRingOfSets_setY d T.
 
 Let m0 : measurable set0.
 Proof.
@@ -986,14 +986,14 @@ HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD.
 
 HB.end.
 
-HB.factory Record isAlgebraOfSets (d : measure_display) T of Pointed T := {
+HB.factory Record isAlgebraOfSets (d : measure_display) T & Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
   measurableC : setC_closed measurable
 }.
 
-HB.builders Context d T of isAlgebraOfSets d T.
+HB.builders Context d T & isAlgebraOfSets d T.
 
 Lemma mD : setD_closed measurable.
 Proof.
@@ -1011,13 +1011,13 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
-HB.factory Record isAlgebraOfSets_setD (d : measure_display) T of Pointed T := {
+HB.factory Record isAlgebraOfSets_setD (d : measure_display) T & Pointed T := {
   measurable : set (set T) ;
   measurableT : measurable [set: T] ;
   measurableD : setD_closed measurable
 }.
 
-HB.builders Context d T of isAlgebraOfSets_setD d T.
+HB.builders Context d T & isAlgebraOfSets_setD d T.
 
 Let m0 : measurable set0.
 Proof. by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed.
@@ -1035,15 +1035,15 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
-HB.factory Record isMeasurable (d : measure_display) T of Pointed T := {
+HB.factory Record isMeasurable (d : measure_display) T & Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableC : forall A, measurable A -> measurable (~` A) ;
   measurable_bigcup : forall F : (set T)^nat, (forall i, measurable (F i)) ->
     measurable (\bigcup_i (F i))
 }.
 
-HB.builders Context d T of isMeasurable d T.
+HB.builders Context d T & isMeasurable d T.
 
 Obligation Tactic := idtac.