Adapt to rocq-prover/rocq#21611

Adapt to rocq-prover/rocq#21611

Author: proux01

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/functions.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.

classical/set_interval.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))

experimental_reals/distr.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/constructive_ereal.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/reals.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}.

reals/signed.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/charge.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
 }.