Adapt to math-comp/math-comp#1110

Author: proux01

_CoqProject

@@ -38,3 +38,5 @@ theories/wielandt_fixpoint.v
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
+# introduced in Rocq 9.2
+-arg -w -arg +level-tolerance

theories/BGsection10.v

@@ -36,9 +36,12 @@ 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" (format "M `_ \alpha").
-Reserved Notation "M `_ \beta" (format "M `_ \beta").
-Reserved Notation "M `_ \sigma" (format "M `_ \sigma").
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "M `_ \alpha" (left associativity, format "M `_ \alpha").
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "M `_ \beta" (left associativity, format "M `_ \beta").
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "M `_ \sigma" (left associativity, format "M `_ \sigma").
 
 Section Def.
 

theories/BGsection13.v

@@ -620,7 +620,7 @@ have{sCMbP_H rFH cPH} piFHs: s \in \pi('F(H)).
 without loss{bH} bMs: L u U M q Q maxM maxL notMGL notLGM t1Mp t1Lp sPM sPL
                nQP nUP regPQ regPU sNQL sNUM hypQ hypU hallH / s \in \beta(M).
 - move=> IH; have:= pnatPpi bH (piSg (Fitting_sub H) piFHs).
-  case/orP; [apply: IH hypQ hypU hallH | apply: IH hypU hypQ _] => //.
+  (case/orP; [apply: IH hypQ hypU hallH | apply: IH hypU hypQ _]) => //.
   by apply: etrans (eq_pHall _ _ _) hallH => ?; apply: orbC.
 without loss{bML_CMbP} sCMbP_H: H hallH piFHs / 'C_(M`_\beta)(P) \subset H.
   have [x cPx sCMbP_Hx] := Hall_subJ solCP hallH (subsetIr _ _) (bML_CMbP M L).

theories/BGsection15.v

@@ -26,6 +26,9 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "M `_ \F" (left associativity, format "M `_ \F").
+
 Section Definitions.
 
 Variables (gT : finGroupType) (M : {set gT}).
@@ -36,7 +39,7 @@ Canonical Structure Fitting_core_group := [group of Fitting_core].
 
 End Definitions.
 
-Notation "M `_ \F" := (Fitting_core M) (format "M `_ \F") : group_scope.
+Notation "M `_ \F" := (Fitting_core M) : group_scope.
 Notation "M `_ \F" := (Fitting_core_group M) : Group_scope.
 
 Section FittingCore.
@@ -1348,7 +1351,7 @@ have defL': L^`(1) = L`_\sigma.
     by rewrite (trivg_kappa maxL hallKs) //; case/setDP: PmaxL.
   suffices ->: Us :=: 1 by rewrite sdprodg1.
   by apply/eqP; rewrite (trivg_kappa_compl maxL complUs).
-have [ntK sKLs']: K :!=: 1 /\ K \subset L`_\sigma^`(1).
+have [ntK sKLs']: K :!=: 1 /\ K \subset (L`_\sigma)^`(1).
   by rewrite -defL' -defK; case/Ptype_cyclics: hallKs.
 have [sQL qQ _] := and3P sylQ.
 have not_cQQ: ~~ abelian Q.

theories/BGsection16.v

@@ -85,6 +85,9 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "M `_ \s" (left associativity, format "M `_ \s").
+
 Section GeneralDefinitions.
 
 Variable gT : finGroupType.
@@ -195,7 +198,7 @@ Definition mmax_transversal U := orbit_transversal 'JG U 'M.
 
 End Definitions.
 
-Notation "M `_ \s" := (FTcore M) (format "M `_ \s") : group_scope.
+Notation "M `_ \s" := (FTcore M) : group_scope.
 Notation "M `_ \s" := (FTcore_group M) : Group_scope.
 
 Notation "''A1' ( M )" := (FTsupport1 M) (format "''A1' ( M )") : group_scope.

theories/PFsection10.v

@@ -1193,7 +1193,7 @@ Qed.
 (* This is the remainder of Peterfalvi (10.11). *)
 Lemma FTtypeII_prime_facts M U W W1 W2 (defW : W1 \x W2 = W) (maxM : M \in 'M) :
     of_typeP M U defW -> FTtype M == 2 ->
-    let H := M`_\F%G in let HU := M^`(1)%G in
+    let H := (M`_\F)%G in let HU := M^`(1)%G in
     let calS := seqIndD HU M H 1 in let tau := FT_Dade0 maxM in
     let p := #|W2| in let q := #|W1| in
   [/\ p.-abelem H, (#|H| = p ^ q)%N & coherent calS M^# tau].

theories/PFsection11.v

@@ -72,7 +72,7 @@ Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
 Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
-Local Notation H := `M`_\F%G.
+Local Notation H := (`M`_\F)%G.
 Local Notation "` 'H'" := `M`_\F : group_scope.
 Local Notation HU := M^`(1)%G.
 Local Notation "` 'HU'" := `M^`(1)%g : group_scope.

theories/PFsection12.v

@@ -40,7 +40,7 @@ Variable L : {group gT}.
 Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).
 
 Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
-Local Notation H := `L`_\F%G.
+Local Notation H := (`L`_\F)%G.
 Local Notation "` 'H'" := `L`_\F : group_scope.
 
 Let nsHL : H <| L. Proof. exact: gFnormal. Qed.
@@ -235,7 +235,7 @@ Local Notation Rgen := FTtype1_subcoherent.
 (* This is Peterfalvi (12.3) *)
 Lemma FTtype1_seqInd_ortho L1 L2 (maxL1 : L1 \in 'M) (maxL2 : L2 \in 'M)
     (L1type1 : FTtype L1 == 1%N) (L2type1 : FTtype L2 == 1%N)
-    (H1 := L1`_\F%G) (H2 := L2`_\F%G)
+    (H1 := (L1`_\F)%G) (H2 := (L2`_\F)%G)
     (calS1 := seqIndD H1 L1 H1 1) (calS2 := seqIndD H2 L2 H2 1)
     (R1 := sval (Rgen maxL1 L1type1)) (R2 := sval (Rgen maxL2 L2type1)) :
     gval L2 \notin L1 :^: G ->
@@ -306,7 +306,7 @@ Variable L : {group gT}.
 Hypothesis maxL : L \in 'M .
 
 Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
-Local Notation H := `L`_\F%G.
+Local Notation H := (`L`_\F)%G.
 Local Notation "` 'H'" := `L`_\F : group_scope.
 Local Notation H' := H^`(1)%G.
 Local Notation "` 'H''" := `H^`(1) : group_scope.
@@ -540,7 +540,7 @@ Hypothesis IHp :
 
 Variables M P0 : {group gT}.
 
-Let K := M`_\F%G.
+Let K := (M`_\F)%G.
 Let K' := K^`(1)%G.
 Let nsKM : K <| M. Proof. exact: gFnormal. Qed.
 
@@ -624,7 +624,7 @@ Hypotheses (maxL : L \in 'M) (sP0_Ls : P0 \subset L`_\s).
 Hypotheses (P0_1s_x : x \in 'Ohm_1(P0)^#) (not_sCxK' : ~~ ('C_K[x] \subset K')).
 Hypotheses (sNxM : 'N(<[x]>) \subset M) (not_sCxL : ~~ ('C[x] \subset L)).
 
-Let H := L`_\F%G.
+Let H := (L`_\F)%G.
 Local Notation "` 'H'" := (gval L)`_\F (format "` 'H'").
 Let nsHL : H <| L. Proof. exact: gFnormal. Qed.
 
@@ -1314,7 +1314,7 @@ have{partGpi exMG} kge2: (k >= 2)%N.
   have /eqP defMG: [set L] == 'M^G by rewrite eqEcard sub1set MG_L cards1.
   have [x] := exMG M maxM; rewrite -defMG => /set1P/(canRL (actK 'JG _))-> /=.
   by rewrite FTcoreJ cardJg FTcore_type1.
-pose L (i : 'I_k) : {group gT} := enum_val i; pose H i := (L i)`_\F%G.
+pose L (i : 'I_k) : {group gT} := enum_val i; pose H i := ((L i)`_\F)%G.
 have MG_L i: L i \in 'M^G by apply: enum_valP.
 have maxL i: L i \in 'M by apply: maxMG.
 have defH i: (L i)`_\s = H i by rewrite FTcore_type1 ?allT1.

theories/PFsection13.v

@@ -84,7 +84,7 @@ Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
 Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
-Local Notation P := `S`_\F%G.
+Local Notation P := (`S`_\F)%G.
 Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
 Local Notation "` 'PU'" := `S^`(1) : group_scope.
@@ -874,7 +874,7 @@ Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
 Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
-Local Notation P := `S`_\F%G.
+Local Notation P := (`S`_\F)%G.
 Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
 Local Notation "` 'PU'" := `S^`(1) : group_scope.
@@ -1590,7 +1590,7 @@ Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
 Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
-Local Notation P := `S`_\F%G.
+Local Notation P := (`S`_\F)%G.
 Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
 Local Notation "` 'PU'" := `S^`(1) : group_scope.
@@ -1950,7 +1950,7 @@ Variable L : {group gT}.
 Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).
 
 Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
-Local Notation H := `L`_\F%G.
+Local Notation H := (`L`_\F)%G.
 Local Notation "` 'H'" := `L`_\F : group_scope.
 
 Let e :=  #|L : H|.

theories/PFsection14.v

@@ -51,13 +51,13 @@ Variables (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).
 Hypotheses (defW : W1 \x W2 = W) (xdefW : W2 \x W1 = W) (maxL : L \in 'M).
 
 Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
-Local Notation P := `S`_\F%G.
+Local Notation P := (`S`_\F)%G.
 Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
 Local Notation "` 'PU'" := `S^`(1)%g : group_scope.
 Local Notation "` 'L'" := (gval L) (only parsing).
-Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F%g (format "` 'H'") : group_scope.
+Local Notation H := (`L`_\F)%G.
+Local Notation "` 'H'" := (`L`_\F)%g (format "` 'H'") : group_scope.
 
 Let p := #|W2|.
 Let q := #|W1|.
@@ -293,8 +293,8 @@ Let ddL := FT_DadeF_hyp maxL.
 Let ddM := FT_DadeF_hyp maxM.
 Let tauL := Dade ddL.
 Let tauM := Dade ddM.
-Let H := L`_\F%G.
-Let K := M`_\F%G.
+Let H := (L`_\F)%G.
+Let K := (M`_\F)%G.
 Let calL := seqIndD H L H 1.
 Let calM := seqIndD K M K 1.
 Let u : algC := #|L : H|%:R.
@@ -381,14 +381,14 @@ Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation What := (cyclicTIset defW).
 
 Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
-Local Notation P := `S`_\F%G.
+Local Notation P := (`S`_\F)%G.
 Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
 Local Notation "` 'PU'" := `S^`(1) : group_scope.
 Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 
 Local Notation "` 'T'" := (gval T) (only parsing) : group_scope.
-Local Notation Q := `T`_\F%G.
+Local Notation Q := (`T`_\F)%G.
 Local Notation "` 'Q'" := `T`_\F : group_scope.
 Local Notation QV := T^`(1)%G.
 Local Notation "` 'QV'" := `T^`(1) : group_scope.
@@ -493,8 +493,8 @@ Let Stype2 := FTtypeP_max_typeII.
 (* These correspond to Peterfalvi, Hypothesis (14.3). *)
 Variables (L : {group gT}) (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).
 Local Notation "` 'L'" := (gval L) (only parsing).
-Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F%g (format "` 'H'") : group_scope.
+Local Notation H := (`L`_\F)%G.
+Local Notation "` 'H'" := (`L`_\F)%g (format "` 'H'") : group_scope.
 
 Hypothesis maxNU_L : L \in 'M('N(U)).
 
@@ -857,8 +857,8 @@ Variables (M : {group gT}) (tau1M : {additive 'CF(M) -> 'CF(G)}) (psi : 'CF(M)).
 Hypothesis maxNV_M : M \in 'M('N(V)).
 
 Local Notation "` 'M'" := (gval M) (only parsing).
-Local Notation K := `M`_\F%G.
-Local Notation "` 'K'" := `M`_\F%g (format "` 'K'") : group_scope.
+Local Notation K := (`M`_\F)%G.
+Local Notation "` 'K'" := (`M`_\F)%g (format "` 'K'") : group_scope.
 
 (* Consequences of the above. *)
 Hypotheses (maxM : M \in 'M) (sNVM : 'N(V) \subset M).