From 276ab5733aa1520383c3dd1a3211b51618b52ed7 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 17 Feb 2026 15:13:09 +0100
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21611

Adapt to https://github.com/rocq-prover/rocq/pull/21611
---
 theories/BGsection7.v | 2 +-
 theories/PFsection2.v | 2 +-
 theories/PFsection3.v | 2 +-
 theories/PFsection4.v | 2 +-
 theories/PFsection9.v | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/BGsection7.v b/theories/BGsection7.v
index 9b48e84..eff2a3b 100644
--- a/theories/BGsection7.v
+++ b/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];
diff --git a/theories/PFsection2.v b/theories/PFsection2.v
index 6193652..3cdfdad 100644
--- a/theories/PFsection2.v
+++ b/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.
diff --git a/theories/PFsection3.v b/theories/PFsection3.v
index 9f32af6..67c06cf 100644
--- a/theories/PFsection3.v
+++ b/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].
diff --git a/theories/PFsection4.v b/theories/PFsection4.v
index 50fa437..a1e6872 100644
--- a/theories/PFsection4.v
+++ b/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}
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index 4597e46..36a4ab0 100644
--- a/theories/PFsection9.v
+++ b/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.