Adapt to math-comp/analysis#1860

Author: proux01

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 *)