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) (at level 0, 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/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.