Adapt to rocq-prover/rocq#17876

Author: proux01

theories/BGsection10.v

@@ -36,9 +36,9 @@ Reserved Notation "\alpha ( M )" (format "\alpha ( M )").
 Reserved Notation "\beta ( M )" (format "\beta ( M )").
 Reserved Notation "\sigma ( M )" (format "\sigma ( M )").
 
-Reserved Notation "M `_ \alpha" (at level 3, format "M `_ \alpha").
-Reserved Notation "M `_ \beta" (at level 3, format "M `_ \beta").
-Reserved Notation "M `_ \sigma" (at level 3, format "M `_ \sigma").
+Reserved Notation "M `_ \alpha" (format "M `_ \alpha").
+Reserved Notation "M `_ \beta" (format "M `_ \beta").
+Reserved Notation "M `_ \sigma" (format "M `_ \sigma").
 
 Section Def.
 

theories/BGsection15.v

@@ -36,8 +36,7 @@ Canonical Structure Fitting_core_group := [group of Fitting_core].
 
 End Definitions.
 
-Notation "M `_ \F" := (Fitting_core M)
-  (at level 3, format "M `_ \F") : group_scope.
+Notation "M `_ \F" := (Fitting_core M) (format "M `_ \F") : group_scope.
 Notation "M `_ \F" := (Fitting_core_group M) : Group_scope.
 
 Section FittingCore.

theories/BGsection16.v

@@ -195,7 +195,7 @@ Definition mmax_transversal U := orbit_transversal 'JG U 'M.
 
 End Definitions.
 
-Notation "M `_ \s" := (FTcore M) (at level 3, format "M `_ \s") : group_scope.
+Notation "M `_ \s" := (FTcore M) (format "M `_ \s") : group_scope.
 Notation "M `_ \s" := (FTcore_group M) : Group_scope.
 
 Notation "''A1' ( M )" := (FTsupport1 M) (format "''A1' ( M )") : group_scope.
@@ -205,7 +205,7 @@ Notation "''A' ( M )" := (FTsupport M) (format "''A' ( M )") : group_scope.
 Notation "''A0' ( M )" := (FTsupport0 M) (format "''A0' ( M )") : group_scope.
 
 Notation "''M^' G" := (mmax_transversal G)
-  (at level 3, format "''M^' G") : group_scope.
+  (at level 1, format "''M^' G") : group_scope.
 
 Section Section16.
 

theories/BGsection2.v

@@ -220,7 +220,7 @@ Let E2_ i t :=
 
 Local Notation "''V_' i" := (V_ i) (at level 8, i at level 2, format "''V_' i").
 Local Notation "''n_' i" := (n_ i) (at level 8, i at level 2, format "''n_' i").
-Local Notation "''E_' i" := (E_ i) (at level 8, i at level 2, format "''E_' i").
+Local Notation "''E_' i" := (E_ i) (i at level 2, format "''E_' i").
 Local Notation "'E_ ( i )" := (E_ i) (only parsing).
 Local Notation "e ^g" := (g^-1 *m (e *m g)) (format "e ^g") : ring_scope.
 Local Notation "'E_ ( i , t )" := (E2_ i t) (format "''E_' ( i ,  t )").

theories/BGsection7.v

@@ -2,7 +2,7 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
-From mathcomp Require Import choice fintype bigop prime finset.
+From mathcomp Require Import choice fintype bigop prime finset finalg mxabelem.
 From mathcomp Require Import fingroup morphism automorphism quotient action.
 From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal hall.
@@ -46,7 +46,6 @@ Import GroupScope.
 
 Reserved Notation "''M'" (format "''M'").
 Reserved Notation "''M' ( H )" (format "''M' ( H )").
-Reserved Notation "''U'".
 Reserved Notation "''SCN_' n [ p ]" (n at level 2, format "''SCN_' n [ p ]").
 Reserved Notation "|/|_ X ( A ; pi )"
   (X at level 2, format "|/|_ X ( A ;  pi )").

theories/PFsection3.v

@@ -442,9 +442,9 @@ Lemma RmodelP (m : model) : is_Rmodel m. Proof. by case: m. Qed.
 
 Fact nil_RmodelP : is_Rmodel nil. Proof. by []. Qed.
 
-Definition eval_cl (m : model) kvs := \sum_(kv <- kvs) m`_kv.1 *~ kv.2.
+Definition eval_cl (m : model) kvs := \sum_(kv <- kvs) m`_(kv.1) *~ kv.2.
 
-Definition sat_lit (m : model) ij kv := '[m ij, m`_kv.1] == kv.2%:~R.
+Definition sat_lit (m : model) ij kv := '[m ij, m`_(kv.1)] == kv.2%:~R.
 Definition sat_cl m cl := uniq (unzip1 cl.2) && all (sat_lit m cl.1) cl.2.
 
 Definition sat (m : model) th :=
@@ -1242,7 +1242,7 @@ have /dIrrP[dk Ddk]: m`_0 \in dirr G.
   have [[/andP[/allP n1m _] Zm] [_ m_gt0 _]] := (RmodelP m, and3P m_th).
   by rewrite dirrE Zm ?[_ == 1]n1m ?mem_nth.
 exists dk => [][i j] /andP[/= lti ltj]; apply/eqP.
-suffices{dk Ddk}: sat_cl m (& (Lit 1 (j == 0))%N in (i, j)).
+suffices{dk Ddk}: sat_cl m (& ((Lit 1 (j == 0))%N) in (i, j)).
   by rewrite /sat_cl /= andbT /sat_lit Ddk.
 without loss{i lti} ->: m i ltj m_th / i = 0%N.
   have [bb21_m m_gt0 m11_x1 m21_x1 _] := and5P m_th.

theories/PFsection9.v

@@ -312,7 +312,7 @@ Proof.
 by have:= typeII_IV_core => /=; case: ifP => // _ [/def_Ptype_factor_prime].
 Qed.
 
-Let frobUW1c : [Frobenius U <*> W1 / C = Ubar ><| W1 / C].
+Let frobUW1c : [Frobenius U <*> W1 / C = Ubar ><| (W1 / C)].
 Proof.
 apply: Frobenius_quotient frobUW1 _ nsCUW1 _.
   by apply: nilpotent_sol; have [_ []] := MtypeP.