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

refinements/examples/irred.v

@@ -32,7 +32,7 @@ Record npolynomial : predArgType := Npolynomial {
 HB.instance Definition _ := [isSub of npolynomial for poly_of_npoly].
 HB.instance Definition _ := [Choice of pos by <:].
 
-Definition npoly_of of (phant R) := npolynomial.
+Definition npoly_of & (phant R) := npolynomial.
 Local Notation npoly_ofR := (npoly_of (Phant R)).
 
 HB.instance Definition _ := SubType.on npoly_ofR.

theory/coherent.v

@@ -20,7 +20,7 @@ Delimit Scope mxpresentation_scope with MP.
 Local Open Scope mxpresentation_scope.
 
 (** Coherent rings *)
-HB.mixin Record Ring_isCoherent R of GRing.Ring R := {
+HB.mixin Record Ring_isCoherent R & GRing.Ring R := {
   dim_ker : forall m n, 'M[R]_(m,n) -> nat;
   ker : forall m n (M : 'M_(m,n)), 'M_(dim_ker _ _ M,m);
   kerP_subproof : forall m n (M : 'M_(m,n)) (X : 'rV_m),
@@ -310,7 +310,7 @@ Qed.
 (*    the underlying ring (in this case a strongly discrete ring) is an *)
 (*    integral domain *)
 HB.factory Record StronglyDiscrete_isIntersectionCoherent R
-           of StronglyDiscrete R := {
+           & StronglyDiscrete R := {
   (** The size of the intersection - 1, this is done to ensure that *)
   (*    the intersection is nonempty *)
   dim_cap : forall m n, 'cV[R]_m -> 'cV[R]_n -> nat;
@@ -319,7 +319,7 @@ HB.factory Record StronglyDiscrete_isIntersectionCoherent R
   cap_spec : forall n m (I : 'cV[R]_n) (J : 'cV[R]_m), int_spec (cap _ _ I J)
 }.
 
-HB.builders Context R of StronglyDiscrete_isIntersectionCoherent R.
+HB.builders Context R & StronglyDiscrete_isIntersectionCoherent R.
 
 Fixpoint dim_int n : 'cV[R]_n -> nat :=
   if n is p.+1 then

theory/dvdring.v

@@ -45,7 +45,7 @@ Variant div_spec (R : ringType) (a b : R) : option R -> Type :=
 | DivDvd x of a = x * b : div_spec a b (Some x)
 | DivNDvd of (forall x, a != x * b) : div_spec a b None.
 
-HB.mixin Record Ring_hasDiv R of GRing.Ring R := {
+HB.mixin Record Ring_hasDiv R & GRing.Ring R := {
   div : R -> R -> option R;
   div_subdef : forall a b, div_spec a b (div a b)
 }.
@@ -589,7 +589,7 @@ End DvdRingTheory.
 (* Notation "x %|d y" := (dvdqr x y) *)
 (*   (at level 40, left associativity, format "x  %|d  y"). *)
 
-HB.mixin Record DvdRing_hasGcd R of DvdRing R := {
+HB.mixin Record DvdRing_hasGcd R & DvdRing R := {
   gcdr : R -> R -> R;
   gcdr_subdef : forall d a b, d %| gcdr a b = (d %| a) && (d %| b)
 }.
@@ -1134,7 +1134,7 @@ End GCDDomainTheory.
 Variant bezout_spec (R : gcdDomainType) (a b : R) : R * R -> Type:=
   BezoutSpec x y of gcdr a b %= x * a + y * b : bezout_spec a b (x, y).
 
-HB.mixin Record GcdDomain_hasPreBezout R of GcdDomain R := {
+HB.mixin Record GcdDomain_hasPreBezout R & GcdDomain R := {
   bezout : R -> R -> (R * R);
   bezout_subdef : forall a b, bezout_spec a b (bezout a b)
 }.
@@ -1384,12 +1384,12 @@ End Bezout_mx.
 
 End BezoutDomainTheory.
 
-HB.factory Record GcdDomain_hasBezout R of GcdDomain R := {
+HB.factory Record GcdDomain_hasBezout R & GcdDomain R := {
   bezout : R -> R -> (R * R);
   bezout_subdef : forall a b, bezout_spec a b (bezout a b)
 }.
 
-HB.builders Context R of GcdDomain_hasBezout R.
+HB.builders Context R & GcdDomain_hasBezout R.
 
 HB.instance Definition _ := GcdDomain_hasPreBezout.Build R bezout_subdef.
 
@@ -1447,7 +1447,7 @@ HB.end.
 
 (* End Mixins. *)
 
-HB.mixin Record DvdRing_isWellFounded R of DvdRing R := {
+HB.mixin Record DvdRing_isWellFounded R & DvdRing R := {
   sdvdr_wf : well_founded (@sdvdr [the dvdRingType of R])
 }.
 
@@ -1477,7 +1477,7 @@ Variant edivr_spec (R : ringType)
   EdivrSpec q r of a = q * b + r & (b != 0) ==> (norm r < norm b)
   : edivr_spec norm a b (q,r).
 
-HB.mixin Record Ring_isEuclidean R of GRing.Ring R := {
+HB.mixin Record Ring_isEuclidean R & GRing.Ring R := {
   enorm : R -> nat;
   ediv : R -> R -> (R * R);
   norm_mul : forall a b, a != 0 -> enorm b <= enorm (a * b);
@@ -1600,14 +1600,14 @@ Qed.
 End Dvd.
 End Dvd.
 
-HB.factory Record IntegralDomain_isEuclidean R of GRing.IntegralDomain R := {
+HB.factory Record IntegralDomain_isEuclidean R & GRing.IntegralDomain R := {
   enorm : R -> nat;
   ediv : R -> R -> (R * R);
   norm_mul : forall a b, a != 0 -> enorm b <= enorm (a * b);
   edivP : forall a b, edivr_spec enorm a b (ediv a b)
 }.
 
-HB.builders Context R of IntegralDomain_isEuclidean R.
+HB.builders Context R & IntegralDomain_isEuclidean R.
 
   Implicit Type a b : [the idomainType of R].
 

theory/edr.v

@@ -26,7 +26,7 @@ Variant smith_spec (R : dvdRingType) m n M
                      & P \in unitmx
                      & Q \in unitmx : smith_spec M (P,d,Q).
 
-HB.mixin Record Bezout_Coherent_isEDR R of DvdRing R := {
+HB.mixin Record Bezout_Coherent_isEDR R & DvdRing R := {
   smith : forall m n, 'M[R]_(m,n) -> 'M[R]_m * seq R * 'M[R]_n;
   smithP : forall m n (M : 'M[R]_(m,n)), smith_spec M (smith _ _ M)
 }.
@@ -44,12 +44,12 @@ Notation "[ 'edrType' 'of' T ]" := (EDR.clone T _)
 Arguments smith {_} [_ _].
 Arguments smithP {_} [_ _].
 
-HB.factory Record DvdRing_isEDR R of DvdRing R := {
+HB.factory Record DvdRing_isEDR R & DvdRing R := {
   smith : forall m n, 'M[R]_(m,n) -> 'M[R]_m * seq R * 'M[R]_n;
   smithP : forall m n (M : 'M[R]_(m,n)), smith_spec M (smith _ _ M)
 }.
 
-HB.builders Context R of DvdRing_isEDR R.
+HB.builders Context R & DvdRing_isEDR R.
 
 Definition smith_seq m n (M : 'M[R]_(m,n)) := (smith M).1.2.
 

theory/fpmod.v

@@ -38,7 +38,7 @@ Record fpmod := FPmod {
   pres  : 'M[R]_(nbrel, nbgen)
 }.
 
-Definition fpmod_of of phant R := fpmod.
+Definition fpmod_of & phant R := fpmod.
 (* Identity Coercion type_fpmod_of : fpmod_of >-> fpmod. *) (* Is this necessary? *)
 
 (* We want morphism_of_rect so temporarily add this: *)

theory/kaplansky.v

@@ -586,21 +586,21 @@ Qed.
 
 End AdequacyEDR.
 
-HB.factory Record BezoutDomain_isAdequacyEDR R of BezoutDomain R := {
+HB.factory Record BezoutDomain_isAdequacyEDR R & BezoutDomain R := {
   gdco : R -> R -> R;
   gdcoP : forall p q, gdco_spec p q (gdco p q)
 }.
 
-HB.builders Context R of BezoutDomain_isAdequacyEDR R.
+HB.builders Context R & BezoutDomain_isAdequacyEDR R.
   HB.instance Definition _ := DvdRing_isEDR.Build R (gdco_smithP gdcoP).
 HB.end.
 
-HB.factory Record BezoutDomain_isKrull1EDR R of BezoutDomain R := {
+HB.factory Record BezoutDomain_isKrull1EDR R & BezoutDomain R := {
   krull1 : forall a u : [the bezoutDomainType of R],
     exists m v, a %| u ^+ m * (1 - u * v)
 }.
 
-HB.builders Context R of BezoutDomain_isKrull1EDR R.
+HB.builders Context R & BezoutDomain_isKrull1EDR R.
 
 Implicit Types a b u : [the bezoutDomainType of R].
 

theory/smith.v

@@ -278,7 +278,7 @@ Qed.
 
 End smith.
 
-HB.factory Record hasSmith E of EuclideanDomain E := {
+HB.factory Record hasSmith E & EuclideanDomain E := {
   find1 : forall m n, 'M[E]_(m.+1,n.+1) -> E -> option 'I_m;
   find2 : forall m n, 'M[E]_(m.+1,n.+1) -> E -> option ('I_(1+m) * 'I_n);
   find_pivot :
@@ -291,7 +291,7 @@ HB.factory Record hasSmith E of EuclideanDomain E := {
     pick_spec [pred ij | E ij.1 ij.2 != 0] (find_pivot _ _ E)
 }.
 
-HB.builders Context E of hasSmith E.
+HB.builders Context E & hasSmith E.
 
 HB.instance Definition _ := DvdRing_isEDR.Build E
   (SmithP find1P find2P find_pivotP).

theory/smithpid.v

@@ -32,7 +32,7 @@ Local Open Scope ring_scope.
 For any i j s.t. ~~ g %| M i j, xrow 0 i M, bezout step on the first row
 and back to 1) *)
 
-HB.factory Record SmithPID R of PID R := {
+HB.factory Record SmithPID R & PID R := {
   find1 : forall m n, 'M[R]_(m.+1,n.+1) -> R -> option 'I_m;
   find2 : forall m n, 'M[R]_(m.+1,n.+1) -> R -> option ('I_(1 + m) * 'I_n);
   find1P : forall m n (M : 'M[R]_(1 + m,1 + n)) a,
@@ -45,7 +45,7 @@ HB.factory Record SmithPID R of PID R := {
     pick_spec [pred ij | M ij.1 ij.2 != 0] (find_pivot _ _ M)
 }.
 
-HB.builders Context R of SmithPID R.
+HB.builders Context R & SmithPID R.
 
 (* This lemma is used in the termination proof of improve_pivot_rec *)
 Lemma sdvd_Bezout_step2 m n i j u' vM (M : 'M[R]_(1 + m, 1 + n)) :

theory/stronglydiscrete.v

@@ -22,7 +22,7 @@
 | Member J of x%:M = J *m I : member_spec x I (Some J)
 | NMember of (forall J, x%:M != J *m I) : member_spec x I None.
 
-HB.mixin Record Ring_isStronglyDiscrete R of GRing.Ring R := {
+HB.mixin Record Ring_isStronglyDiscrete R & GRing.Ring R := {
   member : forall n, R -> 'cV_n -> option 'rV_n;
   member_specP : forall n (x : R) (I : 'cV_n), member_spec x I (member n x I)
 }.
@@ -62,7 +62,7 @@
 Definition subid m n (I : 'cV[R]_m) (J : 'cV[R]_n) : bool :=
   [forall i, member (I i 0) J].
 
 Arguments subid m%nat_scope n%nat_scope I%ideal_scope J%ideal_scope.
 Prenex Implicits subid.
 Local Notation "A <= B" := (subid A B) : ideal_scope.
 Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%IS : ideal_scope.