Merge pull request math-comp#77 from proux01/rocq21611

Adapt to rocq-prover/rocq#21611

Author: proux01

theories/BGsection7.v

@@ -53,7 +53,7 @@ Reserved Notation "|/|* ( A ; pi )" (format "|/|* ( A ;  pi )").
 
 (* The generic setup for the whole Odd Order Theorem proof. *)
 
-HB.mixin Record IsMinSimpleOddGroup gT of FinGroup gT := {
+HB.mixin Record IsMinSimpleOddGroup gT & FinGroup gT := {
   mFT_odd_full : odd #|[set: gT]|;
   mFT_simple : simple [set: gT];
   mFT_nonSolvable : ~~ solvable [set: gT];

theories/PFsection2.v

@@ -103,7 +103,7 @@ Qed.
 
 Fact Dade_signalizer_key : unit. Proof. by []. Qed.
 Definition Dade_signalizer_def a := 'O_pi^'('C_G[a])%G.
-Definition Dade_signalizer of Dade_hypothesis G L A :=
+Definition Dade_signalizer & Dade_hypothesis G L A :=
   locked_with Dade_signalizer_key Dade_signalizer_def.
 
 Hypothesis ddA : Dade_hypothesis G L A.

theories/PFsection3.v

@@ -65,7 +65,7 @@ Section Definitions.
 
 Variables (gT : finGroupType) (G W W1 W2 : {set gT}).
 
-Definition cyclicTIset of W1 \x W2 = W := W :\: (W1 :|: W2).
+Definition cyclicTIset & W1 \x W2 = W := W :\: (W1 :|: W2).
 
 Definition cyclicTI_hypothesis (defW : W1 \x W2 = W) :=
   [/\ cyclic W, odd #|W| & normedTI (cyclicTIset defW) G W].

theories/PFsection4.v

@@ -139,7 +139,7 @@ by case/and3P=> _ _ /andP[] /andP[] /eqP.
 Qed.
 
 (* This is Peterfalvi, Hypothesis (4.2), with explicit parameters. *)
-Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
+Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) & W1 \x W2 = W :=
   [/\ (*a*) [/\ K ><| W1 = L, W1 != 1, Hall L W1 & cyclic W1],
       (*b*) [/\ W2 != 1, W2 \subset K & cyclic W2],
             {in W1^#, forall x, 'C_K[x] = W2}

theories/PFsection9.v

@@ -144,7 +144,7 @@ by rewrite -(@leq_pmul2l (p ^ q)) -?oH ?cUW2 //= expn_gt0 cardG_gt0.
 Qed.
 
 (* Existential witnesses for Peterfalvi (9.4). *)
-Definition Ptype_Fcore_kernel of of_typeP M U defW :=
+Definition Ptype_Fcore_kernel & of_typeP M U defW :=
   odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0].
 Let H0 := (Ptype_Fcore_kernel MtypeP).
 Local Notation "` 'H0'" := (gval H0) (only parsing) : group_scope.