diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 99c60f144f..664dbf4ee8 100644
--- a/classical/classical_sets.v
+++ b/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.
diff --git a/classical/filter.v b/classical/filter.v
index 5df3835ca8..0d2f6d45f1 100644
--- a/classical/filter.v
+++ b/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.
diff --git a/classical/functions.v b/classical/functions.v
index 38cf34e941..21961e61b9 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -253,7 +253,7 @@ Notation "{ 'oinv' aT >-> rT }" := (@OInversible.type aT rT) : type_scope.
 Notation "[ 'oinv'  'of'  f ]" := [the {oinv _ >-> _} of f : _ -> _] :
   form_scope.
 Definition phant_oinv aT rT (f : {oinv aT >-> rT})
-  of phantom (_ -> _) f := @oinv _ _ f.
+  & phantom (_ -> _) f := @oinv _ _ f.
 Notation "''oinv_' f" := (@phant_oinv _ _ _ (Phantom (_ -> _) f%FUN)).
 
 HB.structure Definition OInvFun aT rT A B :=
@@ -262,13 +262,13 @@ Notation "{ 'oinvfun' A >-> B }" := (@OInvFun.type _ _ A B) : type_scope.
 Notation "[ 'oinvfun'  'of'  f ]" :=
   [the {oinvfun _ >-> _} of f : _ -> _] : form_scope.
 
-HB.mixin Record OInv_Inv {aT rT} (f : aT -> rT) of OInv _ _ f := {
+HB.mixin Record OInv_Inv {aT rT} (f : aT -> rT) & OInv _ _ f := {
   inv : rT -> aT;
   oliftV : olift inv = 'oinv_f
 }.
 
 HB.factory Record Inv {aT rT} (f : aT -> rT) := { inv : rT -> aT  }.
-HB.builders Context {aT rT} (f : aT -> rT) of Inv _ _ f.
+HB.builders Context {aT rT} (f : aT -> rT) & Inv _ _ f.
   HB.instance Definition _ := OInv.Build _ _ f (olift inv).
   HB.instance Definition _ := OInv_Inv.Build _ _ f erefl.
 HB.end.
@@ -276,7 +276,7 @@ HB.end.
 HB.structure Definition Inversible aT rT := {f of Inv aT rT f}.
 Notation "{ 'inv' aT >->  rT }" := (@Inversible.type aT rT) : type_scope.
 Notation "[ 'inv'  'of'  f ]" := [the {inv _ >-> _} of f : _ -> _] : form_scope.
-Definition phant_inv aT rT (f : {inv aT >-> rT}) of phantom (_ -> _) f :=
+Definition phant_inv aT rT (f : {inv aT >-> rT}) & phantom (_ -> _) f :=
   @inv _ _ f.
 Notation "f ^-1" := (@inv _ _ f%function) (only printing) : function_scope.
 Notation "f ^-1" :=
@@ -292,7 +292,7 @@ Notation "[ 'invfun'  'of'  f ]" :=
   [the {invfun _ >-> _} of f : _ -> _] : form_scope.
 
 HB.mixin Record OInv_CanV {aT rT} {A : set aT} {B : set rT}
-  (f : aT -> rT) of OInv _ _ f := {
+  (f : aT -> rT) & OInv _ _ f := {
     oinvS : {homo 'oinv_f : x / B x >-> (some @` A) x};
     oinvK : {in B, ocancel 'oinv_f f};
   }.
@@ -302,7 +302,7 @@ HB.factory Record OCanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) := {
           oinvK : {in B, ocancel oinv f};
   }.
 HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT)
-   of OCanV _ _ A B f.
+   & OCanV _ _ A B f.
  HB.instance Definition _ := OInv.Build _ _ f oinv.
  HB.instance Definition _ := OInv_CanV.Build _ _ A B f oinvS oinvK.
 HB.end.
@@ -331,7 +331,7 @@ Notation "{ 'splitsurjfun' A >-> B }" :=
 Notation "[ 'splitsurjfun'  'of'  f ]" :=
   [the {splitsurjfun _ >-> _} of f : _ -> _] : form_scope.
 
-HB.mixin Record OInv_Can aT rT (A : set aT) (f : aT -> rT) of OInv _ _ f :=
+HB.mixin Record OInv_Can aT rT (A : set aT) (f : aT -> rT) & OInv _ _ f :=
   { funoK : {in A, pcancel f 'oinv_f} }.
 
 HB.structure Definition Inject aT rT A :=
@@ -393,7 +393,7 @@ End ShortFunSyntax.
 (******************************************************************************)
 
 Definition phant_funS aT rT (A : set aT) (B : set rT)
-  (f : {fun A >-> B}) of phantom (_ -> _) f := @funS _ _ _ _ f.
+  (f : {fun A >-> B}) & phantom (_ -> _) f := @funS _ _ _ _ f.
 Notation "'funS_  f" := (phant_funS (Phantom (_ -> _) f))
   (at level 8, f at level 2) : form_scope.
 #[global] Hint Extern 0 (set_fun _ _ _) => solve [apply: funS] : core.
@@ -409,7 +409,7 @@ Definition mem_fun aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) :=
 #[global] Hint Extern 0 (prop_in1 _ _) => solve [apply: mem_fun] : core.
 
 Definition phant_mem_fun aT rT (A : set aT) (B : set rT)
-  (f : {fun A >-> B}) of phantom (_ -> _) f := homo_setP.2 (@funS _ _ _ _ f).
+  (f : {fun A >-> B}) & phantom (_ -> _) f := homo_setP.2 (@funS _ _ _ _ f).
 Notation "'mem_fun_  f" := (phant_mem_fun (Phantom (_ -> _) f))
   (at level 8, f at level 2) : form_scope.
 
@@ -417,12 +417,12 @@ Lemma some_inv {aT rT} (f : {inv aT >-> rT}) x : Some (f^-1 x) = 'oinv_f x.
 Proof. by rewrite -oliftV. Qed.
 
 Definition phant_oinvK aT rT (A : set aT) (B : set rT)
-   (f : {surj A >-> B}) of phantom (_ -> _) f := @oinvK _ _ _ _ f.
+   (f : {surj A >-> B}) & phantom (_ -> _) f := @oinvK _ _ _ _ f.
 Notation "'oinvK_ f" := (phant_oinvK (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve oinvK : core.
 
 Definition phant_oinvS aT rT (A : set aT) (B : set rT)
-   (f : {surj A >-> B}) of phantom (_ -> _) f := @oinvS _ _ _ _ f.
+   (f : {surj A >-> B}) & phantom (_ -> _) f := @oinvS _ _ _ _ f.
 Notation "'oinvS_ f" := (phant_oinvS (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve oinvS : core.
 
@@ -438,7 +438,7 @@ by have /cid2 [x Ax <-] := 'oinvS_f By => <-; constructor.
 Qed.
 
 Definition phant_oinvP aT rT (A : set aT) (B : set rT)
-   (f : {surj A >-> B}) of phantom (_ -> _) f := @oinvP _ _ _ _ f.
+   (f : {surj A >-> B}) & phantom (_ -> _) f := @oinvP _ _ _ _ f.
 Notation "'oinvP_ f" := (phant_oinvP (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve oinvP : core.
 
@@ -446,7 +446,7 @@ Lemma oinvT {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}} x :
   B x -> 'oinv_f x.
 Proof. by move=> /'oinvS_f [a Aa <-]. Qed.
 Definition phant_oinvT aT rT (A : set aT) (B : set rT)
-   (f : {surj A >-> B}) of phantom (_ -> _) f := @oinvT _ _ _ _ f.
+   (f : {surj A >-> B}) & phantom (_ -> _) f := @oinvT _ _ _ _ f.
 Notation "'oinvT_ f" := (phant_oinvT (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve oinvT : core.
 
@@ -454,7 +454,7 @@ Lemma invK {aT rT} {A : set aT} {B : set rT} {f : {splitsurj A >-> B}} :
    {in B, cancel f^-1 f}.
 Proof. by move=> x Bx; rewrite -[x in RHS]'oinvK_f// -some_inv/=. Qed.
 Definition phant_invK aT rT (A : set aT) (B : set rT)
-   (f : {splitsurj A >-> B}) of phantom (_ -> _) f := @invK _ _ _ _ f.
+   (f : {splitsurj A >-> B}) & phantom (_ -> _) f := @invK _ _ _ _ f.
 Notation "'invK_ f" := (phant_invK (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve invK : core.
 
@@ -462,18 +462,18 @@ Lemma invS {aT rT} {A : set aT} {B : set rT} {f : {splitsurj A >-> B}} :
   {homo f^-1 : x / B x >-> A x}.
 Proof. by move=> x /'oinvS_f/= [a Aa]; rewrite -some_inv => -[<-]. Qed.
 Definition phant_invS aT rT (A : set aT) (B : set rT)
-   {f : {splitsurjfun A >-> B}} of phantom (_ -> _) f := @invS _ _ _ _ f.
+   {f : {splitsurjfun A >-> B}} & phantom (_ -> _) f := @invS _ _ _ _ f.
 Notation "'invS_ f" := (phant_invS (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve invS : core.
 
 Definition phant_funoK aT rT (A : set aT) (f : {inj A >-> rT})
-  of phantom (_ -> _) f := @funoK _ _ _ f.
+  & phantom (_ -> _) f := @funoK _ _ _ f.
 Notation "'funoK_ f" := (phant_funoK (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve funoK : core.
 
 Definition inj {aT rT : nonPropType} {A : set aT} {f : {inj A >-> rT}} :
    {in A &, injective f} := pcan_in_inj funoK.
-Definition phant_inj aT rT (A : set aT) (f : {inj A >-> rT}) of
+Definition phant_inj aT rT (A : set aT) (f : {inj A >-> rT}) &
    phantom (_ -> _) f := @inj _ _ _ f.
 Notation "'inj_ f" := (phant_inj (Phantom (_ -> _) f)) : form_scope.
 
@@ -491,7 +491,7 @@ Lemma funK {aT rT : Type} {A : set aT} {s : {splitinj A >-> rT}} :
 Proof. by move=> x Ax; apply: Some_inj; rewrite some_inv funoK. Qed.
 
 Definition phant_funK aT rT (A : set aT) (f : {splitinj A >-> rT})
-  of phantom (_ -> _) f := @funK _ _ _ f.
+  & phantom (_ -> _) f := @funK _ _ _ f.
 Notation "'funK_  f" := (phant_funK (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Resolve funK : core.
 
@@ -508,21 +508,21 @@ Qed.
 
 (** Preliminary Builders *)
 
-HB.factory Record Inv_Can {aT rT} {A : set aT} (f : aT -> rT) of Inv _ _ f :=
+HB.factory Record Inv_Can {aT rT} {A : set aT} (f : aT -> rT) & Inv _ _ f :=
   { funK : {in A, cancel f f^-1} }.
-HB.builders Context {aT rT} A (f : aT -> rT) of @Inv_Can _ _ A f.
+HB.builders Context {aT rT} A (f : aT -> rT) & @Inv_Can _ _ A f.
   Local Lemma funoK: {in A, pcancel f 'oinv_f}.
   Proof. by rewrite -oliftV/=; apply: can_in_pcan; apply: funK. Qed.
   HB.instance Definition _ := OInv_Can.Build _ _ A f funoK.
 HB.end.
 
 HB.factory Record Inv_CanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT)
-     of Inv aT rT f := {
+     & Inv aT rT f := {
   invS : {homo f^-1 : x / B x >-> A x};
   invK : {in B, cancel f^-1 f};
 }.
 HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT)
-    of Inv_CanV _ _ A B f.
+    & Inv_CanV _ _ A B f.
   #[local] Lemma oinvK : {in B, ocancel 'oinv_f f}.
   Proof. by move=> x Bx; rewrite -some_inv/= invK. Qed.
   #[local] Lemma oinvS : {homo 'oinv_f : x / B x >-> (some @` A) x}.
@@ -787,12 +787,12 @@ End Map.
 
 HB.factory Record CanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) :=
   { inv; invS : {homo inv : x / B x >-> A x}; invK : {in B, cancel inv f}; }.
-HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of CanV _ _ A B f.
+HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) & CanV _ _ A B f.
  HB.instance Definition _ := Inv.Build _ _ f inv.
  HB.instance Definition _ := Inv_CanV.Build _ _ _ _ f invS invK.
 HB.end.
 
-HB.factory Record OInv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.factory Record OInv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
   @OInv _ _ f :=
   {
     funS :  {homo f : x / A x >-> B x};
@@ -800,7 +800,7 @@ HB.factory Record OInv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
     funoK : {in A, pcancel f 'oinv_f};
     oinvK : {in B, ocancel 'oinv_f f};
   }.
-HB.builders Context {aT rT} A B (f : aT -> rT) of OInv_Can2 _ _ A B f.
+HB.builders Context {aT rT} A B (f : aT -> rT) & OInv_Can2 _ _ A B f.
   HB.instance Definition _ := isFun.Build aT rT _ _ f funS.
   HB.instance Definition _ := OInv_Can.Build aT rT _ f funoK.
   HB.instance Definition _ := OInv_CanV.Build aT rT _ _ f oinvS oinvK.
@@ -812,7 +812,7 @@ HB.factory Record OCan2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) :=
            funoK : {in A, pcancel f oinv};
            oinvK : {in B, ocancel oinv f};
    }.
-HB.builders Context {aT rT} A B (f : aT -> rT) of OCan2 _ _ A B f.
+HB.builders Context {aT rT} A B (f : aT -> rT) & OCan2 _ _ A B f.
   HB.instance Definition _ := OInv.Build aT rT f oinv.
   HB.instance Definition _ := OInv_Can2.Build aT rT _ _ f funS oinvS funoK oinvK.
 HB.end.
@@ -820,19 +820,19 @@ HB.end.
 
 HB.factory Record Can {aT rT} {A : set aT} (f : aT -> rT) :=
   { inv; funK : {in A, cancel f inv} }.
-HB.builders Context {aT rT} A (f : aT -> rT) of @Can _ _ A f. (* bug if swap f and A *)
+HB.builders Context {aT rT} A (f : aT -> rT) & @Can _ _ A f. (* bug if swap f and A *)
  HB.instance Definition _ := Inv.Build _ _ f inv.
  HB.instance Definition _ := Inv_Can.Build _ _ _ f funK.
 HB.end.
 
-HB.factory Record Inv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.factory Record Inv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
    Inv _ _ f :=
    { funS : {homo f : x / A x >-> B x};
      invS : {homo f^-1 : x / B x >-> A x};
      funK : {in A, cancel f f^-1};
      invK : {in B, cancel f^-1 f};
    }.
-HB.builders Context {aT rT} A B (f : aT -> rT) of Inv_Can2 _ _ A B f.
+HB.builders Context {aT rT} A B (f : aT -> rT) & Inv_Can2 _ _ A B f.
   HB.instance Definition _ := isFun.Build aT rT A B f funS.
   HB.instance Definition _ := Inv_Can.Build aT rT A f funK.
   HB.instance Definition _ := @Inv_CanV.Build aT rT A B f invS invK.
@@ -844,15 +844,15 @@ HB.factory Record Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) :=
          funK : {in A, cancel f inv};
          invK : {in B, cancel inv f};
    }.
-HB.builders Context {aT rT} A B (f : aT -> rT) of Can2 _ _ A B f.
+HB.builders Context {aT rT} A B (f : aT -> rT) & Can2 _ _ A B f.
   HB.instance Definition _ := Inv.Build aT rT f inv.
   HB.instance Definition _ := Inv_Can2.Build aT rT A B f funS invS funK invK.
 HB.end.
 
-HB.factory Record SplitInjFun_CanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.factory Record SplitInjFun_CanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
      @SplitInjFun _ _ A B f :=
   { invS : {homo f^-1 : x / B x >-> A x}; injV : {in B &, injective f^-1} }.
-HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of SplitInjFun_CanV _ _ A B f.
+HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) & SplitInjFun_CanV _ _ A B f.
   Let mem_inv := homo_setP.2 invS.
   Local Lemma invK : {in B, cancel f^-1 f}.
   Proof. by move=> x Bx; apply: injV; rewrite ?funK ?(mem_fun, mem_inv). Qed.
@@ -860,7 +860,7 @@ HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of SplitInj
 HB.end.
 
 HB.factory Record BijTT {aT rT} (f : aT -> rT) := { bij : bijective f }.
-HB.builders Context {aT rT} f of BijTT aT rT f.
+HB.builders Context {aT rT} f & BijTT aT rT f.
   Local Lemma exg : {g | cancel f g /\ cancel g f}.
   Proof. by apply: cid; case: bij => g; exists g. Qed.
   HB.instance Definition _ := Can2.Build aT rT setT setT f
@@ -910,7 +910,7 @@ Lemma surj {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}} : set_surj A B
 Proof. by move=> b /'oinvP_f[x Ax _]; exists x. Qed.
 
 Definition phant_surj aT rT (A : set aT) (B : set rT) (f : {surj A >-> B})
-  of phantom (_ -> _) f := @surj _ _ _ _ f.
+  & phantom (_ -> _) f := @surj _ _ _ _ f.
 Notation "'surj_  f" := (phant_surj (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Extern 0 (set_surj _ _ _) => solve [apply: surj] : core.
 
@@ -976,7 +976,7 @@ Notation split := 'split_(fun=> point).
 
 HB.factory Record Inj {aT rT} (A : set aT) (f : aT -> rT) :=
    { inj : {in A &, injective f} }.
-HB.builders Context {aT rT} A (f : aT -> rT) of Inj _ _ A f.
+HB.builders Context {aT rT} A (f : aT -> rT) & Inj _ _ A f.
   HB.instance Definition _ := OInversible.copy f [fun f in A].
   Lemma funoK : {in A, pcancel f 'oinv_f}.
   Proof.
@@ -987,9 +987,9 @@ HB.builders Context {aT rT} A (f : aT -> rT) of Inj _ _ A f.
   HB.instance Definition _ := OInv_Can.Build _ _ _ f funoK.
 HB.end.
 
-HB.factory Record SurjFun_Inj {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.factory Record SurjFun_Inj {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
    @SurjFun _ _ A B f := { inj : {in A &, injective f} }.
-HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
     @SurjFun_Inj _ _ A B f.
   Let g := f.
   HB.instance Definition _ := Inj.Build _ _ A g inj.
@@ -1001,10 +1001,10 @@ HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
  HB.instance Definition _ := fcan.
 HB.end.
 
-HB.factory Record SplitSurjFun_Inj {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.factory Record SplitSurjFun_Inj {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
      @SplitSurjFun _ _ A B f :=
    { inj : {in A &, injective f} }.
-HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of
+HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) &
     @SplitSurjFun_Inj _ _ A B f.
   Local Lemma funK : {in A, cancel f f^-1%FUN}.
   Proof.  by move=> x Ax; apply: inj; rewrite ?invK ?mem_fun. Qed.
@@ -1477,7 +1477,7 @@ HB.instance Definition _ n := SplitBij.copy (@IIord n) (ordII^-1).
 (******************************************************************************)
 
 Definition glue {T T'} {X Y : set T} {A B : set T'}
-  of [disjoint X & Y] & [disjoint A & B] :=
+  & [disjoint X & Y] & [disjoint A & B] :=
   fun (f g : T -> T') (u : T) => if u \in X then f u else g u.
 
 Section Glue12.
@@ -1774,7 +1774,7 @@ Qed.
 
 Section set_bij_lemmas.
 Context {aT rT : Type} {A : set aT} {B : set rT} {f : aT -> rT}.
-Definition fun_set_bij of set_bij A B f := f.
+Definition fun_set_bij & set_bij A B f := f.
 Context (fbij : set_bij A B f).
 Local Notation g := (fun_set_bij fbij).
 
@@ -1806,7 +1806,7 @@ Coercion bij_of_set_bijection : set_bij >-> Bij.type.
 
 Lemma bij {aT rT} {A : set aT} {B : set rT} {f : {bij A >-> B}} : set_bij A B f.
 Proof. split=> //. Qed.
-Definition phant_bij aT rT (A : set aT) (B : set rT) (f : {bij A >-> B}) of
+Definition phant_bij aT rT (A : set aT) (B : set rT) (f : {bij A >-> B}) &
   phantom (_ -> _) f := @bij _ _ _ _ f.
 Notation "''bij_' f" := (phant_bij (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Extern 0 (set_bij _ _ _) => solve [apply: bij] : core.
@@ -1831,7 +1831,7 @@ Qed.
 Lemma bijTT {aT rT}  {f : {bij [set: aT] >-> [set: rT]}} : bijective f.
 Proof. by rewrite -setTT_bijective. Qed.
 Definition phant_bijTT aT rT (f : {bij [set: aT] >-> [set: rT]})
-   of phantom (_ -> _) f := @bijTT _ _ f.
+   & phantom (_ -> _) f := @bijTT _ _ f.
 Notation "''bijTT_'  f" := (phant_bijTT (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Extern 0 (bijective _) => solve [apply: bijTT] : core.
 
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 7008aadd0f..e0d26aaa63 100644
--- a/classical/set_interval.v
+++ b/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.
diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v
index f1c9708cc3..37fe02f40a 100644
--- a/experimental_reals/distr.v
+++ b/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))
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 93cf4d82b5..14eba026af 100644
--- a/reals/constructive_ereal.v
+++ b/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)
diff --git a/reals/reals.v b/reals/reals.v
index 0ec78136a6..1a6685839d 100644
--- a/reals/reals.v
+++ b/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),
diff --git a/reals/signed.v b/reals/signed.v
index 4dc5e44a65..5ea28aea9a 100644
--- a/reals/signed.v
+++ b/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}.
diff --git a/theories/charge.v b/theories/charge.v
index a26756493b..7f1a4f6b12 100644
--- a/theories/charge.v
+++ b/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.
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 8f7bab2e18..1b9d045c96 100644
--- a/theories/hoelder.v
+++ b/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
 }.
 
diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v
index c5df28f3e6..3b739b1492 100644
--- a/theories/homotopy_theory/continuous_path.v
+++ b/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;
 }.
diff --git a/theories/kernel.v b/theories/kernel.v
index af531ec353..2eaa9643c5 100644
--- a/theories/kernel.v
+++ b/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.
diff --git a/theories/landau.v b/theories/landau.v
index 18ed51ff34..fcb35f7c62 100644
--- a/theories/landau.v
+++ b/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).
 
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index 7f0d773d3b..422a97b530 100644
--- a/theories/measurable_realfun.v
+++ b/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).
diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v
index 2866461f8a..91c1e89efb 100644
--- a/theories/measure_theory/measurable_structure.v
+++ b/theories/measure_theory/measurable_structure.v
@@ -866,7 +866,7 @@ 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
 }.
 
@@ -874,7 +874,7 @@ HB.mixin Record SemiRingOfSets_isRingOfSets d T of SemiRingOfSets d T := {
 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]
 }.
 
@@ -882,12 +882,12 @@ HB.mixin Record RingOfSets_isAlgebraOfSets d T of RingOfSets d T := {
 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,7 +903,7 @@ 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 ;
@@ -911,7 +911,7 @@ HB.factory Record isSigmaRing (d : measure_display) T of Pointed T := {
     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,7 +1035,7 @@ 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) ;
@@ -1043,7 +1043,7 @@ HB.factory Record isMeasurable (d : measure_display) T of Pointed T := {
     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.
 
diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v
index 1db0086dd2..d82dee0498 100644
--- a/theories/measure_theory/measure_extension.v
+++ b/theories/measure_theory/measure_extension.v
@@ -122,7 +122,7 @@ HB.factory Record isSubsetOuterMeasure
   subset_outer_measure_sigma_subadditive :
     forall A F, subset_sigma_subadditive mu A F}.
 
-HB.builders Context {R : realType} T mu of isSubsetOuterMeasure R T mu.
+HB.builders Context {R : realType} T mu & isSubsetOuterMeasure R T mu.
 
 Lemma le_outer_measure : {homo mu : A B / A `<=` B >-> A <= B}.
 Proof.
diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index 8324cef378..e564c1302b 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -422,7 +422,7 @@ End content_on_ring_of_sets.
 Hint Resolve measureU measure_bigsetU : core.
 
 HB.mixin Record Content_isMeasure d (T : semiRingOfSetsType d)
-    (R : numFieldType) (mu : set T -> \bar R) of Content d mu := {
+    (R : numFieldType) (mu : set T -> \bar R) & Content d mu := {
   measure_semi_sigma_additive : semi_sigma_additive mu }.
 
 #[short(type=measure)]
@@ -458,7 +458,7 @@ HB.factory Record isMeasure d (T : semiRingOfSetsType d) (R : realFieldType)
   measure_semi_sigma_additive : semi_sigma_additive mu }.
 
 HB.builders Context d (T : semiRingOfSetsType d) (R : realFieldType)
-  (mu : set T -> \bar R) of isMeasure _ T R mu.
+  (mu : set T -> \bar R) & isMeasure _ T R mu.
 
 Let semi_additive_mu : semi_additive mu.
 Proof.
@@ -1121,11 +1121,11 @@ End ring_sigma_subadditive_content.
 
 #[key="mu"]
 HB.factory Record Content_SigmaSubAdditive_isMeasure d (R : realType)
-    (T : semiRingOfSetsType d) (mu : set T -> \bar R) of Content d mu := {
+    (T : semiRingOfSetsType d) (mu : set T -> \bar R) & Content d mu := {
   measure_sigma_subadditive : measurable_subset_sigma_subadditive mu }.
 
 HB.builders Context d (R : realType) (T : semiRingOfSetsType d)
-  (mu : set T -> \bar R) of Content_SigmaSubAdditive_isMeasure d R T mu.
+  (mu : set T -> \bar R) & Content_SigmaSubAdditive_isMeasure d R T mu.
 
 HB.instance Definition _ := Content_isMeasure.Build d T R mu
   (semiring_sigma_additive (measure_sigma_subadditive)).
@@ -1369,11 +1369,11 @@ Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" :=
   (sigma_finite_measure T R) : ring_scope.
 
 HB.factory Record Measure_isSigmaFinite d (T : measurableType d)
-    (R : realType) (mu : set T -> \bar R) of isMeasure _ _ _ mu :=
+    (R : realType) (mu : set T -> \bar R) & isMeasure _ _ _ mu :=
   { sigma_finiteT : sigma_finite setT mu }.
 
 HB.builders Context d (T : measurableType d) (R : realType)
-  mu of @Measure_isSigmaFinite d T R mu.
+  mu & @Measure_isSigmaFinite d T R mu.
 
 Lemma sfinite : sfinite_measure mu.
 Proof. exact/sfinite_measure_sigma_finite/sigma_finiteT. Qed.
@@ -1413,10 +1413,10 @@ Notation "{ 'finite_measure' 'set' T '->' '\bar' R }" :=
 
 HB.factory Record Measure_isFinite d (T : measurableType d)
     (R : realType) (k : set T -> \bar R)
-  of isMeasure _ _ _ k := { fin_num_measure : fin_num_fun k }.
+  & isMeasure _ _ _ k := { fin_num_measure : fin_num_fun k }.
 
 HB.builders Context d (T : measurableType d) (R : realType) k
-  of Measure_isFinite d T R k.
+  & Measure_isFinite d T R k.
 
 Let sfinite : sfinite_measure k.
 Proof.
@@ -1473,12 +1473,12 @@ HB.instance Definition _ := @Measure_isFinite.Build _ T _ scale fin_num_scale.
 End finite_mscale.
 
 HB.factory Record Measure_isSFinite d (T : sigmaRingType d)
-    (R : realType) (k : set T -> \bar R) of isMeasure _ _ _ k := {
+    (R : realType) (k : set T -> \bar R) & isMeasure _ _ _ k := {
   s_finite : exists s : {finite_measure set T -> \bar R}^nat,
     forall U, measurable U -> k U = mseries s 0 U }.
 
 HB.builders Context d (T : sigmaRingType d) (R : realType)
-  k of Measure_isSFinite d T R k.
+  k & Measure_isSFinite d T R k.
 
 Let sfinite : sfinite_measure k.
 Proof.
@@ -1527,7 +1527,7 @@ Qed.
 End sfinite_measure.
 
 Definition mfrestr d (T : measurableType d) (R : realFieldType) (D : set T)
-    (f : set T -> \bar R) (mD : measurable D) of (f D < +oo)%E :=
+    (f : set T -> \bar R) (mD : measurable D) & (f D < +oo)%E :=
   mrestr f mD.
 
 Section measure_frestr.
diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v
index 46a04c39ee..1ad06c84f5 100644
--- a/theories/measure_theory/probability_measure.v
+++ b/theories/measure_theory/probability_measure.v
@@ -54,11 +54,11 @@ HB.structure Definition SubProbability d (T : measurableType d) (R : realType)
   := {mu of @FiniteMeasure d T R mu & isSubProbability d T R mu }.
 
 HB.factory Record Measure_isSubProbability d (T : measurableType d)
-    (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P :=
+    (R : realType) (P : set T -> \bar R) & isMeasure _ _ _ P :=
   { sprobability_setT : (P setT <= 1)%E }.
 
 HB.builders Context d (T : measurableType d) (R : realType)
-  P of Measure_isSubProbability d T R P.
+  P & Measure_isSubProbability d T R P.
 
 Let finite : @Measure_isFinite d T R P.
 Proof.
@@ -114,11 +114,11 @@ Qed.
 End probability_lemmas.
 
 HB.factory Record Measure_isProbability d (T : measurableType d)
-    (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P :=
+    (R : realType) (P : set T -> \bar R) & isMeasure _ _ _ P :=
   { probability_setT : P setT = 1%E }.
 
 HB.builders Context d (T : measurableType d) (R : realType)
-  P of Measure_isProbability d T R P.
+  P & Measure_isProbability d T R P.
 
 Let subprobability : @Measure_isSubProbability d T R P.
 Proof. by split; rewrite probability_setT. Qed.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index e6fe7b6c9b..9bf04bb6e3 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -77,7 +77,7 @@ Local Open Scope ring_scope.
 (** Modules with a norm depending on a numDomain *)
 
 HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V
-    of PseudoMetricNormedZmod K V & Tvs K V := {
+    & PseudoMetricNormedZmod K V & Tvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
@@ -87,11 +87,11 @@ HB.structure Definition NormedModule (K : numDomainType) :=
    & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
 
 HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V
-    of PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
+    & PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
  normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
-HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
+HB.builders Context K V & PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
 
 (* NB: These lemmas are done later with more machinery. They should
    be simplified once normedtype is split, and the present section can
@@ -279,14 +279,14 @@ End pseudoMetric_from_normedZmodType.
 Export pseudoMetric_from_normedZmodType.Exports.
 
 HB.factory Record Lmodule_isNormed (R : numFieldType) M
-    of GRing.Lmodule R M := {
+    & GRing.Lmodule R M := {
  norm : M -> R;
  ler_normD : forall x y, norm (x + y) <= norm x + norm y ;
  normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ;
  normr0_eq0 : forall x : M, norm x = 0 -> x = 0
 }.
 
-HB.builders Context R M of Lmodule_isNormed R M.
+HB.builders Context R M & Lmodule_isNormed R M.
 
 Lemma normrMn x n : norm (x *+ n) = norm x *+ n.
 Proof.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 7edbaecb9e..76844f9b64 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -125,7 +125,7 @@ Unshelve. all: by end_near. Qed.
 End at_left_right_topologicalType.
 
 HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
-    of Num.NormedZmodule R T & PseudoPointedMetric R T := {
+    & Num.NormedZmodule R T & PseudoPointedMetric R T := {
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
 }.
 
@@ -136,11 +136,11 @@ HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
 
 (* alternative definition of a PseudoMetricNormedZmod *)
 HB.factory Record NormedZmoduleMetric (R : numDomainType) T
-    of Num.NormedZmodule R T & Metric R T & isPointed T := {
+    & Num.NormedZmodule R T & Metric R T & isPointed T := {
   mdist_norm : forall x y : T, mdist x y = `|y - x|
 }.
 
-HB.builders Context (R : numDomainType) T of NormedZmoduleMetric R T.
+HB.builders Context (R : numDomainType) T & NormedZmoduleMetric R T.
 
 Let pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |).
 Proof.
diff --git a/theories/numfun.v b/theories/numfun.v
index 1079b0eeb2..4a678cd1d7 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -1070,7 +1070,7 @@ End comring.
 HB.factory Record FiniteDecomp (T : pointedType) (R : nzRingType) (f : T -> R) :=
   { fimfunE : exists (r : seq R) (A_ : R -> set T),
       forall x, f x = \sum_(y <- r) (y * \1_(A_ y) x) }.
-HB.builders Context T R f of @FiniteDecomp T R f.
+HB.builders Context T R f & @FiniteDecomp T R f.
   Lemma finite_subproof: @FiniteImage T R f.
   Proof.
   split; have [r [A_ fE]] := fimfunE.
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 992f0e1272..dcbfbd40ad 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -939,7 +939,7 @@ Qed.
 End markov_chebyshev_cantelli.
 
 HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d)
-    (T' : measurableType d') (X : T -> T') of @MeasurableFun d d' T T' X := {
+    (T' : measurableType d') (X : T -> T') & @MeasurableFun d d' T T' X := {
   countable_range : countable (range X)
 }.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index 52f168ea92..b93e3d31cd 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1013,7 +1013,7 @@ Lemma is_cvg_geometric_series (R : archiRealFieldType) (a z : R) : `|z| < 1 ->
 Proof. by move=> /cvg_geometric_series/cvgP; apply. Qed.
 
 Definition normed_series_of (K : numDomainType) (V : normedModType K)
-    (u_ : V ^nat) of phantom V^nat (series u_) : K ^nat :=
+    (u_ : V ^nat) & phantom V^nat (series u_) : K ^nat :=
   [series `|u_ n|]_n.
 Notation "[ 'normed' s_ ]" := (@normed_series_of _ _ _ (Phantom _ s_)) : ring_scope.
 Arguments normed_series_of {K V} u_ _ n /.
diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v
index 9884875d07..26207586da 100644
--- a/theories/topology_theory/discrete_topology.v
+++ b/theories/topology_theory/discrete_topology.v
@@ -29,7 +29,7 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-HB.mixin Record Discrete_ofNbhs T of Nbhs T := {
+HB.mixin Record Discrete_ofNbhs T & Nbhs T := {
   nbhs_principalE : (@nbhs T _) = principal_filter;
 }.
 
@@ -41,14 +41,14 @@ Definition discrete_ent {T} : set (set (T * T)) :=
 
 (** Note: having the discrete topology does not guarantee the discrete
     uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *)
-HB.mixin Record Discrete_ofUniform T of Uniform T := {
+HB.mixin Record Discrete_ofUniform T & Uniform T := {
   uniform_discrete : @entourage T = discrete_ent
 }.
 
 Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop :=
   x = y.
 
-HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
+HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T &
     PseudoMetric R T := {
   metric_discrete : @ball R T = @discrete_ball R T
 }.
@@ -77,7 +77,7 @@ HB.structure Definition DiscreteUniform :=
 HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
   { T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.
 
-HB.builders Context T of Discrete_ofNbhs T.
+HB.builders Context T & Discrete_ofNbhs T.
 
 Local Lemma principal_nbhs_filter (p : T) : ProperFilter (nbhs p).
 Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed.
@@ -94,8 +94,8 @@ HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T
 
 HB.end.
 
-HB.factory Record DiscreteUniform_ofNbhs T of Discrete_ofNbhs T & Nbhs T := {}.
-HB.builders Context T of DiscreteUniform_ofNbhs T.
+HB.factory Record DiscreteUniform_ofNbhs T & Discrete_ofNbhs T & Nbhs T := {}.
+HB.builders Context T & DiscreteUniform_ofNbhs T.
 
 Local Open Scope relation_scope.
 
@@ -140,10 +140,10 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl.
 
 HB.end.
 
-HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
+HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T &
   DiscreteUniform T := {}.
 
-HB.builders Context R T of DiscretePseudoMetric_ofUniform R T.
+HB.builders Context R T & DiscretePseudoMetric_ofUniform R T.
 
 Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
   @discrete_ball R T x eps x.
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index 4b5ffb1bb1..e08ff5e9a5 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -32,7 +32,7 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-HB.mixin Record PseudoMetric_isMetric (K : numDomainType) M of PseudoMetric K M := {
+HB.mixin Record PseudoMetric_isMetric (K : numDomainType) M & PseudoMetric K M := {
   mdist : M -> M -> K ;
   mdist_ge0 : forall x y, 0 <= mdist x y ;
   mdist_positivity : forall x y, mdist x y = 0 -> x = y;
@@ -92,7 +92,7 @@ Qed.
 
 End metric_lemmas.
 
-HB.factory Record isMetric (K : numFieldType) (M : Type) of Choice M := {
+HB.factory Record isMetric (K : numFieldType) (M : Type) & Choice M := {
   mdist : M -> M -> K ;
   mdistxx : forall x, mdist x x = 0 ;
   mdist_positivity : forall x y, mdist x y = 0 -> x = y ;
@@ -100,7 +100,7 @@ HB.factory Record isMetric (K : numFieldType) (M : Type) of Choice M := {
   mdist_triangle : forall y x z, mdist x z <= mdist x y + mdist y z
 }.
 
-HB.builders Context K M of isMetric K M.
+HB.builders Context K M & isMetric K M.
 
 Let ball (x : M) e : set M := [set y | mdist x y < e].
 
diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v
index eafb9197a1..c4d611b390 100644
--- a/theories/topology_theory/order_topology.v
+++ b/theories/topology_theory/order_topology.v
@@ -45,7 +45,7 @@ HB.structure Definition POrderedPointedTopological d :=
   {T of PointedTopological T & Order.isPOrder d T}.
 
 (** TODO: generalize this to a preOrder once that's available *)
-HB.mixin Record Order_isNbhs d (T : Type) of Nbhs T & Order.Total d T := {
+HB.mixin Record Order_isNbhs d (T : Type) & Nbhs T & Order.Total d T := {
   (** Note that just the intervals `]a, b[ doesn't work when the order has a
       top or bottom element, so we also need the rays `]-oo, b[ and ]a, +oo[ *)
   itv_nbhsE : forall x : T, nbhs x = filter_from
diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v
index 2d76d10172..157622bd03 100644
--- a/theories/topology_theory/pseudometric_structure.v
+++ b/theories/topology_theory/pseudometric_structure.v
@@ -64,7 +64,7 @@ Lemma entourage_E {R : numDomainType} {T T'} (ball : T -> R -> set T') :
   @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]).
 Proof. by []. Qed.
 
-HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M of Uniform M := {
+HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M & Uniform M := {
   ball : M -> R -> M -> Prop ;
   ball_center_subproof : forall x (e : R), 0 < e -> ball x e x ;
   ball_sym_subproof : forall x y (e : R), ball x e y -> ball y e x ;
@@ -82,7 +82,7 @@ HB.structure Definition PseudoPointedMetric (R : numDomainType) :=
   {T of Pointed T & Uniform T & Uniform_isPseudoMetric R T}.
 
 (* was uniformityOfBallMixin *)
-HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
+HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M & Nbhs M := {
   ent : set_system (M * M);
   nbhsE : nbhs = nbhs_ ent;
   ball : M -> R -> M -> Prop ;
@@ -93,7 +93,7 @@ HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
   entourageE : ent = entourage_ ball
 }.
 
-HB.builders Context R M of Nbhs_isPseudoMetric R M.
+HB.builders Context R M & Nbhs_isPseudoMetric R M.
 Local Open Scope relation_scope.
 
 Let ball_le x : {homo ball x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index 58e897bd03..232b04c149 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -90,7 +90,7 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
 (** Topological spaces *)
-HB.mixin Record Nbhs_isTopological (T : Type) of Nbhs T := {
+HB.mixin Record Nbhs_isTopological (T : Type) & Nbhs T := {
   open : set_system T;
   nbhs_pfilter_subproof : forall p : T, ProperFilter (nbhs p) ;
   nbhsE_subproof : forall p : T, nbhs p =
@@ -373,7 +373,7 @@ Unshelve. all: by end_near. Qed.
 
 (* [locally P] replaces a (globally A) in P by a within A (nbhs x)      *)
 (* Can be combined with a notation taking a filter as its last argument *)
-Definition locally_of (P : set_system T -> Prop) of phantom Prop (P (globally A))
+Definition locally_of (P : set_system T -> Prop) & phantom Prop (P (globally A))
   := forall x, A x -> P (within A (nbhs x)).
 Local Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).
 (* e.g. [locally [bounded f x | x in A]]                  *)
@@ -419,13 +419,13 @@ Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).
 
 (** Topology defined by a filter *)
 
-HB.factory Record Nbhs_isNbhsTopological T of Nbhs T := {
+HB.factory Record Nbhs_isNbhsTopological T & Nbhs T := {
   nbhs_filter : forall p : T, ProperFilter (nbhs p);
   nbhs_singleton : forall (p : T) (A : set T), nbhs p A -> A p;
   nbhs_nbhs : forall (p : T) (A : set T), nbhs p A -> nbhs p (nbhs^~ A);
 }.
 
-HB.builders Context T of Nbhs_isNbhsTopological T.
+HB.builders Context T & Nbhs_isNbhsTopological T.
 
 Definition open_of_nbhs := [set A : set T | A `<=` nbhs^~ A].
 
@@ -452,7 +452,7 @@ HB.end.
 Definition nbhs_of_open (T : Type) (op : set_system T) (p : T) (A : set T) :=
   exists B, [/\ op B, B p & B `<=` A].
 
-HB.factory Record isOpenTopological T of Choice T := {
+HB.factory Record isOpenTopological T & Choice T := {
   op : set_system T ;
   opT : op setT ;
   opI : forall (A B : set T), op A -> op B -> op (A `&` B) ;
@@ -460,7 +460,7 @@ HB.factory Record isOpenTopological T of Choice T := {
     op (\bigcup_i f i)
 }.
 
-HB.builders Context T of isOpenTopological T.
+HB.builders Context T & isOpenTopological T.
 
 HB.instance Definition _ := hasNbhs.Build T (nbhs_of_open op).
 
@@ -497,7 +497,7 @@ HB.end.
 
 (** Topology defined by a base of open sets *)
 
-HB.factory Record isBaseTopological T of Choice T := {
+HB.factory Record isBaseTopological T & Choice T := {
   I : pointedType;
   D : set I;
   b : I -> (set T);
@@ -506,7 +506,7 @@ HB.factory Record isBaseTopological T of Choice T := {
     exists k, [/\ D k, b k t & b k `<=` b i `&` b j];
 }.
 
-HB.builders Context T of isBaseTopological T.
+HB.builders Context T & isBaseTopological T.
 
 Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
 
@@ -556,13 +556,13 @@ HB.instance Definition _ := isOpenTopological.Build T
 
 HB.end.
 
-HB.factory Record isSubBaseTopological T of Choice T := {
+HB.factory Record isSubBaseTopological T & Choice T := {
   I : pointedType;
   D : set I;
   b : I -> (set T);
 }.
 
-HB.builders Context T of isSubBaseTopological T.
+HB.builders Context T & isSubBaseTopological T.
 
 Local Notation finI_from := (finI_from D b).
 
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 51c439a410..6e7fc18006 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -58,7 +58,7 @@ Proof. by []. Qed.
 
 Local Open Scope relation_scope.
 
-HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := {
+HB.mixin Record Nbhs_isUniform_mixin M & Nbhs M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_diagonal_subproof :
@@ -78,7 +78,7 @@ HB.structure Definition PointedUniform :=
   {T of PointedTopological T & Nbhs_isUniform_mixin T}.
 
 
-HB.factory Record Nbhs_isUniform M of Nbhs M := {
+HB.factory Record Nbhs_isUniform M & Nbhs M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_diagonal : forall A, entourage A -> diagonal `<=` A;
@@ -90,7 +90,7 @@ HB.factory Record Nbhs_isUniform M of Nbhs M := {
 
 Local Close Scope relation_scope.
 
-HB.builders Context M of Nbhs_isUniform M.
+HB.builders Context M & Nbhs_isUniform M.
 
 Let nbhs_filter (p : M) : ProperFilter (nbhs p).
 Proof.
@@ -126,7 +126,7 @@ HB.end.
 
 Local Open Scope relation_scope.
 
-HB.factory Record isUniform M of Choice M := {
+HB.factory Record isUniform M & Choice M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_diagonal : forall A, entourage A -> diagonal `<=` A;
@@ -137,7 +137,7 @@ HB.factory Record isUniform M of Choice M := {
 
 Local Close Scope relation_scope.
 
-HB.builders Context M of isUniform M.
+HB.builders Context M & isUniform M.
 
 HB.instance Definition _ := @hasNbhs.Build M (nbhs_ entourage).
 
@@ -346,7 +346,7 @@ move=> ab [/= /xsectionP Balima /xsectionP Blimb]; apply: sB2A.
 by exists (lim F).
 Qed.
 
-HB.mixin Record Uniform_isComplete T of PointedUniform T := {
+HB.mixin Record Uniform_isComplete T & PointedUniform T := {
   cauchy_cvg :
     forall (F : set_system T), ProperFilter F -> cauchy F -> cvg F
 }.
diff --git a/theories/tvs.v b/theories/tvs.v
index fa1ea5cb43..82daf0d9af 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -81,7 +81,7 @@ HB.structure Definition PreTopologicalNmodule :=
   {M of Topological M & GRing.Nmodule M}.
 
 HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
-    of PreTopologicalNmodule M := {
+    & PreTopologicalNmodule M := {
   add_continuous : continuous (fun x : M * M => x.1 + x.2) ;
 }.
 
@@ -92,7 +92,7 @@ HB.structure Definition PreTopologicalZmodule :=
   {M of Topological M & GRing.Zmodule M}.
 
 HB.mixin Record TopologicalNmodule_isTopologicalZmodule M
-    of Topological M & GRing.Zmodule M := {
+    & Topological M & GRing.Zmodule M := {
   opp_continuous : continuous (-%R : M -> M) ;
 }.
 
@@ -102,11 +102,11 @@ HB.structure Definition TopologicalZmodule :=
         & TopologicalNmodule_isTopologicalZmodule M}.
 
 HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M
-    of Topological M & GRing.Zmodule M := {
+    & Topological M & GRing.Zmodule M := {
   sub_continuous : continuous (fun x : M * M => x.1 - x.2) ;
 }.
 
-HB.builders Context M of PreTopologicalNmodule_isTopologicalZmodule M.
+HB.builders Context M & PreTopologicalNmodule_isTopologicalZmodule M.
 
 Lemma opp_continuous : continuous (-%R : M -> M).
 Proof.
@@ -156,7 +156,7 @@ HB.structure Definition PreTopologicalLmodule (K : numDomainType) :=
   {M of Topological M & GRing.Lmodule K M}.
 
 HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M
-    of Topological M & GRing.Lmodule R M := {
+    & Topological M & GRing.Lmodule R M := {
   scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ;
 }.
 
@@ -166,11 +166,11 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) :=
         & TopologicalZmodule_isTopologicalLmodule K M}.
 
 HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M
-    of Topological M & GRing.Lmodule R M := {
+    & Topological M & GRing.Lmodule R M := {
   scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ;
 }.
 
-HB.builders Context R M of TopologicalNmodule_isTopologicalLmodule R M.
+HB.builders Context R M & TopologicalNmodule_isTopologicalLmodule R M.
 
 Lemma opp_continuous : continuous (-%R : M -> M).
 Proof.
@@ -192,7 +192,7 @@ HB.end.
 
 HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}.
 
-HB.mixin Record PreUniformNmodule_isUniformNmodule M of PreUniformNmodule M := {
+HB.mixin Record PreUniformNmodule_isUniformNmodule M & PreUniformNmodule M := {
   add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2)
 }.
 
@@ -202,7 +202,7 @@ HB.structure Definition UniformNmodule :=
 HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}.
 
 HB.mixin Record UniformNmodule_isUniformZmodule M
-    of Uniform M & GRing.Zmodule M := {
+    & Uniform M & GRing.Zmodule M := {
   opp_unif_continuous : unif_continuous (-%R : M -> M)
 }.
 
@@ -210,11 +210,11 @@ HB.structure Definition UniformZmodule :=
   {M of UniformNmodule M & GRing.Zmodule M & UniformNmodule_isUniformZmodule M}.
 
 HB.factory Record PreUniformNmodule_isUniformZmodule M
-    of Uniform M & GRing.Zmodule M := {
+    & Uniform M & GRing.Zmodule M := {
   sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2)
 }.
 
-HB.builders Context M of PreUniformNmodule_isUniformZmodule M.
+HB.builders Context M & PreUniformNmodule_isUniformZmodule M.
 
 Lemma opp_unif_continuous : unif_continuous (-%R : M -> M).
 Proof.
@@ -277,7 +277,7 @@ HB.structure Definition PreUniformLmodule (K : numDomainType) :=
   {M of Uniform M & GRing.Lmodule K M}.
 
 HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M
-    of PreUniformLmodule R M := {
+    & PreUniformLmodule R M := {
   scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ;
 }.
 
@@ -286,11 +286,11 @@ HB.structure Definition UniformLmodule (R : numFieldType) :=
         & PreUniformLmodule_isUniformLmodule R M}.
 
 HB.factory Record UniformNmodule_isUniformLmodule (R : numFieldType) M
-    of PreUniformLmodule R M := {
+    & PreUniformLmodule R M := {
   scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ;
 }.
 
-HB.builders Context R M of UniformNmodule_isUniformLmodule R M.
+HB.builders Context R M & UniformNmodule_isUniformLmodule R M.
 
 Lemma opp_unif_continuous : unif_continuous (-%R : M -> M).
 Proof.
@@ -321,7 +321,7 @@ Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
   0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A.
 
 HB.mixin Record Uniform_isTvs (R : numDomainType) E
-    of Uniform E & GRing.Lmodule R E := {
+    & Uniform E & GRing.Lmodule R E := {
   locally_convex : exists2 B : set (set E),
     (forall b, b \in B -> convex b) & basis B
 }.
@@ -367,14 +367,14 @@ Unshelve. all: by end_near. Qed.
 End properties_of_topologicalLmodule.
 
 HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E
-    of Topological E & GRing.Lmodule R E := {
+    & Topological E & GRing.Lmodule R E := {
   add_continuous : continuous (fun x : E * E => x.1 + x.2) ;
   scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ;
   locally_convex : exists2 B : set (set E),
     (forall b, b \in B -> convex b) & basis B
   }.
 
-HB.builders Context R E of PreTopologicalLmod_isTvs R E.
+HB.builders Context R E & PreTopologicalLmod_isTvs R E.
 
 Definition entourage : set_system (E * E) :=
   fun P => exists (U : set E), nbhs (0 : E) U  /\