Adapt to https://github.com/math-comp/analysis/pull/1860

theories/BGappendixAB.v

@@ -8,6 +8,7 @@ From mathcomp Require Import center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal.
 From mathcomp Require Import mxrepresentation mxabelem.
 From odd_order Require Import BGsection1 BGsection2.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file contains the useful material in B & G, appendices A and B, i.e., *)

theories/BGappendixC.v

@@ -12,6 +12,7 @@ From mathcomp Require Import frobenius.
 From mathcomp Require Import falgebra fieldext galois algC finfield.
 From mathcomp Require Import mxabelem classfun character integral_char inertia.
 From odd_order Require Import BGsection1.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/BGsection1.v

@@ -8,6 +8,7 @@ From mathcomp Require Import mxalgebra.
 From mathcomp Require Import cyclic center gfunctor commutator finmodule.
 From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
 From mathcomp Require Import hall extremal mxrepresentation mxabelem.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file contains most of the material in B & G, section 1, including the *)

theories/BGsection10.v

@@ -8,6 +8,7 @@ From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal hall.
 From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
 From odd_order Require Import BGsection6 BGsection7 BGsection9.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 10, including with the definitions:      *)

theories/BGsection11.v

@@ -8,6 +8,7 @@ From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal hall.
 From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
 From odd_order Require Import BGsection6 BGsection7 BGsection10.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 11; it has only one definition:          *)

theories/BGsection12.v

@@ -9,6 +9,7 @@ From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
 From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
 From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
 From odd_order Require Import BGsection11.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 12; it defines the prime sets for the    *)

theories/BGsection13.v

@@ -9,6 +9,7 @@ From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
 From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
 From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
 From odd_order Require Import BGsection12.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 13; the title subject of the section,    *)

theories/BGsection14.v

@@ -9,6 +9,7 @@ From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
 From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
 From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
 From odd_order Require Import BGsection12 BGsection13.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 14, starting with the definition of the  *)

theories/BGsection15.v

@@ -9,6 +9,7 @@ From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
 From odd_order Require Import BGsection1 BGsection2 BGsection3 BGsection4.
 From odd_order Require Import BGsection5 BGsection6 BGsection7 BGsection9.
 From odd_order Require Import BGsection10 BGsection12 BGsection13 BGsection14.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 15; it fills in the picture of maximal   *)

theories/BGsection16.v

@@ -10,6 +10,7 @@ From odd_order Require Import BGsection1 BGsection2 BGsection3 BGsection4.
 From odd_order Require Import BGsection5 BGsection6 BGsection7 BGsection9.
 From odd_order Require Import BGsection10 BGsection12 BGsection13 BGsection14.
 From odd_order Require Import BGsection15.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 16; it summarises all the results of the *)

theories/BGsection2.v

@@ -9,6 +9,7 @@ From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal.
 From mathcomp Require Import hall mxrepresentation mxabelem.
 From odd_order Require Import BGsection1.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers the useful material in B & G, Section 2. This excludes    *)

theories/BGsection3.v

@@ -9,6 +9,7 @@ From mathcomp Require Import cyclic center gfunctor commutator finmodule.
 From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
 From mathcomp Require Import hall frobenius extremal mxrepresentation mxabelem.
 From odd_order Require Import wielandt_fixpoint BGsection1 BGsection2.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers the material in B & G, Section 3.                       *)

theories/BGsection4.v

@@ -8,6 +8,7 @@ From mathcomp Require Import cyclic center gfunctor commutator.
 From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
 From mathcomp Require Import hall extremal mxrepresentation mxabelem.
 From odd_order Require Import BGsection1 BGsection2.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, Section 4, i.e., the proof of structure theorems *)

theories/BGsection5.v

@@ -7,6 +7,7 @@ From mathcomp Require Import action gproduct.
 From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal hall.
 From odd_order Require Import BGsection1 BGsection4.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers Section 5 of B & G, except for some technical results   *)

theories/BGsection6.v

@@ -6,6 +6,7 @@ From mathcomp Require Import fingroup morphism automorphism quotient gproduct.
 From mathcomp Require Import cyclic center gfunctor commutator.
 From mathcomp Require Import pgroup nilpotent sylow abelian maximal hall.
 From odd_order Require Import BGsection1 BGappendixAB.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers most of B & G section 6.                                *)

theories/BGsection7.v

@@ -7,6 +7,7 @@ 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.
 From odd_order Require Import BGsection1 BGsection6.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 7, i.e., the proof of the Thompson       *)

theories/BGsection8.v

@@ -6,6 +6,7 @@ From mathcomp Require Import fingroup automorphism action gproduct.
 From mathcomp Require Import center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal.
 From odd_order Require Import BGsection1 BGsection5 BGsection6 BGsection7.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 8, i.e., the proof of two special cases  *)

theories/BGsection9.v

@@ -7,6 +7,7 @@ From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
 From mathcomp Require Import nilpotent sylow abelian maximal hall.
 From odd_order Require Import BGsection1 BGsection4 BGsection5 BGsection6.
 From odd_order Require Import BGsection7 BGsection8.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file covers B & G, section 9, i.e., the proof the Uniqueness        *)

theories/PFsection1.v

@@ -12,6 +12,7 @@ From mathcomp Require Import cyclic center commutator pgroup nilpotent hall.
 From mathcomp Require Import falgebra fieldext galois algC algnum.
 From mathcomp Require Import mxrepresentation classfun character inertia.
 From mathcomp Require Import integral_char vcharacter.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 1: Preliminary results.               *)

theories/PFsection10.v

@@ -16,6 +16,7 @@ From odd_order Require Import BGsection1 BGsection3 BGsection7 BGsection15.
 From odd_order Require Import BGsection16 PFsection1 PFsection2 PFsection3.
 From odd_order Require Import PFsection4 PFsection5 PFsection6 PFsection7.
 From odd_order Require Import PFsection8 PFsection9.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 10: Maximal subgroups of Types III,   *)

theories/PFsection11.v

@@ -16,6 +16,7 @@ From odd_order Require Import BGsection1 BGsection3 BGsection7 BGsection15.
 From odd_order Require Import BGsection16 PFsection1 PFsection2 PFsection3.
 From odd_order Require Import PFsection4 PFsection5 PFsection6 PFsection7.
 From odd_order Require Import PFsection8 PFsection9 PFsection10.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 11: Maximal subgroups of Types        *)

theories/PFsection12.v

@@ -17,6 +17,7 @@ From odd_order Require Import BGsection7 BGsection14 BGsection15 BGsection16.
 From odd_order Require Import PFsection1 PFsection2 PFsection3 PFsection4.
 From odd_order Require Import PFsection5 PFsection6 PFsection7 PFsection8.
 From odd_order Require Import PFsection9 PFsection10 PFsection11.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/PFsection13.v

@@ -17,6 +17,7 @@ From odd_order Require Import BGsection14 BGsection15 BGsection16.
 From odd_order Require Import PFsection1 PFsection2 PFsection3 PFsection4.
 From odd_order Require Import PFsection5 PFsection6 PFsection7 PFsection8.
 From odd_order Require Import PFsection9 PFsection10 PFsection11 PFsection12.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 13: The Subgroups S and T.            *)

theories/PFsection14.v

@@ -17,6 +17,7 @@ From odd_order Require Import BGsection15 BGsection16 BGappendixC PFsection1.
 From odd_order Require Import PFsection2 PFsection3 PFsection4 PFsection5.
 From odd_order Require Import PFsection6 PFsection7 PFsection8 PFsection9.
 From odd_order Require Import PFsection10 PFsection11 PFsection12 PFsection13.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 14: Non_existence of G.               *)

theories/PFsection2.v

@@ -11,6 +11,7 @@ From mathcomp Require Import algC.
 From mathcomp Require Import mxrepresentation classfun character inertia.
 From mathcomp Require Import vcharacter.
 From odd_order Require Import PFsection1.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 2: the Dade isometry                  *)

theories/PFsection3.v

@@ -12,6 +12,7 @@ From mathcomp Require Import falgebra fieldext galois algC algnum.
 From mathcomp Require Import mxrepresentation classfun character integral_char.
 From mathcomp Require Import inertia vcharacter.
 From odd_order Require Import PFsection1 PFsection2.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 3: TI-Subsets with Cyclic Normalizers *)

theories/PFsection4.v

@@ -12,6 +12,7 @@ From mathcomp Require Import hall frobenius algC.
 From mathcomp Require Import mxrepresentation classfun character inertia.
 From mathcomp Require Import vcharacter.
 From odd_order Require Import PFsection1 PFsection2 PFsection3.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 4: The Dade isometry of a certain     *)

theories/PFsection5.v

@@ -11,6 +11,7 @@ From mathcomp Require Import cyclic center gfunctor pgroup frobenius algC.
 From mathcomp Require Import mxrepresentation classfun character inertia.
 From mathcomp Require Import vcharacter.
 From odd_order Require Import PFsection1 PFsection2 PFsection3 PFsection4.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 5: Coherence.                         *)

theories/PFsection6.v

@@ -14,6 +14,7 @@ From mathcomp Require Import mxrepresentation classfun character integral_char.
 From mathcomp Require Import inertia vcharacter.
 From odd_order Require Import PFsection1 PFsection2 PFsection3 PFsection4.
 From odd_order Require Import PFsection5.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 6:                                    *)

theories/PFsection7.v

@@ -14,6 +14,7 @@ From mathcomp Require Import mxrepresentation classfun character inertia.
 From mathcomp Require Import vcharacter.
 From odd_order Require Import BGsection3 PFsection1 PFsection2 PFsection4.
 From odd_order Require Import PFsection5 PFsection6.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 7:                                    *)

theories/PFsection8.v

@@ -13,6 +13,7 @@ From mathcomp Require Import vcharacter.
 From odd_order Require Import BGsection1 BGsection3 BGsection7 BGsection10.
 From odd_order Require Import BGsection14 BGsection15 BGsection16 PFsection1.
 From odd_order Require Import PFsection2 PFsection3 PFsection4 PFsection5.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 8: Structure of a Minimal Simple      *)

theories/PFsection9.v

@@ -16,6 +16,7 @@ From mathcomp Require Import inertia vcharacter.
 From odd_order Require Import BGsection1 BGsection3 BGsection7 BGsection15.
 From odd_order Require Import BGsection16 PFsection1 PFsection2 PFsection3.
 From odd_order Require Import PFsection4 PFsection5 PFsection6 PFsection8.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file covers Peterfalvi, Section 9: On the maximal subgroups of Types  *)

theories/stripped_odd_order_theorem.v

@@ -5,6 +5,7 @@ From mathcomp Require ssreflect ssrfun ssrbool eqtype ssrnat fintype finset.
 From mathcomp Require fingroup morphism quotient action gproduct.
 From mathcomp Require gfunctor commutator gseries nilpotent.
 From odd_order Require PFsection14.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (* This file contains a minimal, self-contained reformulation of the Odd      *)

theories/wielandt_fixpoint.v

@@ -10,6 +10,7 @@ From mathcomp Require Import cyclic center gfunctor commutator finmodule.
 From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
 From mathcomp Require Import hall frobenius extremal mxrepresentation mxabelem.
 From odd_order Require Import BGsection1.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 (******************************************************************************)
 (*   This file provides the proof of the Wielandt fixpoint order formula,     *)