diff --git a/theories/BGappendixAB.v b/theories/BGappendixAB.v
index 5d2fcfa..24e8203 100644
--- a/theories/BGappendixAB.v
+++ b/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., *)
diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v
index 2db24cf..31b2e85 100644
--- a/theories/BGappendixC.v
+++ b/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.
diff --git a/theories/BGsection1.v b/theories/BGsection1.v
index 971d3eb..7723217 100644
--- a/theories/BGsection1.v
+++ b/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 *)
diff --git a/theories/BGsection10.v b/theories/BGsection10.v
index 1b94a8c..df06272 100644
--- a/theories/BGsection10.v
+++ b/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:      *)
diff --git a/theories/BGsection11.v b/theories/BGsection11.v
index 83d108e..c208696 100644
--- a/theories/BGsection11.v
+++ b/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:          *)
diff --git a/theories/BGsection12.v b/theories/BGsection12.v
index d9711f7..d994303 100644
--- a/theories/BGsection12.v
+++ b/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    *)
diff --git a/theories/BGsection13.v b/theories/BGsection13.v
index 7899773..a19914c 100644
--- a/theories/BGsection13.v
+++ b/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,    *)
diff --git a/theories/BGsection14.v b/theories/BGsection14.v
index 61bb73b..1ffb84c 100644
--- a/theories/BGsection14.v
+++ b/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  *)
diff --git a/theories/BGsection15.v b/theories/BGsection15.v
index f83e033..9cfd907 100644
--- a/theories/BGsection15.v
+++ b/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   *)
diff --git a/theories/BGsection16.v b/theories/BGsection16.v
index 481fba5..18aacca 100644
--- a/theories/BGsection16.v
+++ b/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 *)
diff --git a/theories/BGsection2.v b/theories/BGsection2.v
index bc77afa..cf74e23 100644
--- a/theories/BGsection2.v
+++ b/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    *)
diff --git a/theories/BGsection3.v b/theories/BGsection3.v
index d073423..a985016 100644
--- a/theories/BGsection3.v
+++ b/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.                       *)
diff --git a/theories/BGsection4.v b/theories/BGsection4.v
index 8032b46..dc15ffc 100644
--- a/theories/BGsection4.v
+++ b/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 *)
diff --git a/theories/BGsection5.v b/theories/BGsection5.v
index 7493fa2..876f6d8 100644
--- a/theories/BGsection5.v
+++ b/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   *)
diff --git a/theories/BGsection6.v b/theories/BGsection6.v
index 410a5e9..443f13c 100644
--- a/theories/BGsection6.v
+++ b/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.                                *)
diff --git a/theories/BGsection7.v b/theories/BGsection7.v
index eff2a3b..3c62989 100644
--- a/theories/BGsection7.v
+++ b/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       *)
diff --git a/theories/BGsection8.v b/theories/BGsection8.v
index 5fcd0d9..92eebfd 100644
--- a/theories/BGsection8.v
+++ b/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  *)
diff --git a/theories/BGsection9.v b/theories/BGsection9.v
index bb9bba2..0ec8680 100644
--- a/theories/BGsection9.v
+++ b/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        *)
diff --git a/theories/PFsection1.v b/theories/PFsection1.v
index 168fef8..9f2bdd2 100644
--- a/theories/PFsection1.v
+++ b/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.               *)
diff --git a/theories/PFsection10.v b/theories/PFsection10.v
index 6cf052d..0a52b7e 100644
--- a/theories/PFsection10.v
+++ b/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,   *)
diff --git a/theories/PFsection11.v b/theories/PFsection11.v
index 94536ca..3bf50f3 100644
--- a/theories/PFsection11.v
+++ b/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        *)
diff --git a/theories/PFsection12.v b/theories/PFsection12.v
index ef4a6be..6857e6d 100644
--- a/theories/PFsection12.v
+++ b/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.
diff --git a/theories/PFsection13.v b/theories/PFsection13.v
index cc930b0..b19a8f8 100644
--- a/theories/PFsection13.v
+++ b/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.            *)
diff --git a/theories/PFsection14.v b/theories/PFsection14.v
index 71f84de..3ee238e 100644
--- a/theories/PFsection14.v
+++ b/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.               *)
diff --git a/theories/PFsection2.v b/theories/PFsection2.v
index 3cdfdad..fcfe9d2 100644
--- a/theories/PFsection2.v
+++ b/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                  *)
diff --git a/theories/PFsection3.v b/theories/PFsection3.v
index 67c06cf..5d99bd1 100644
--- a/theories/PFsection3.v
+++ b/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 *)
diff --git a/theories/PFsection4.v b/theories/PFsection4.v
index a1e6872..154dcc6 100644
--- a/theories/PFsection4.v
+++ b/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     *)
diff --git a/theories/PFsection5.v b/theories/PFsection5.v
index 8a17fe4..be20e12 100644
--- a/theories/PFsection5.v
+++ b/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.                         *)
diff --git a/theories/PFsection6.v b/theories/PFsection6.v
index 9aaea66..166b9ad 100644
--- a/theories/PFsection6.v
+++ b/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:                                    *)
diff --git a/theories/PFsection7.v b/theories/PFsection7.v
index 1107bae..a68f5fc 100644
--- a/theories/PFsection7.v
+++ b/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:                                    *)
diff --git a/theories/PFsection8.v b/theories/PFsection8.v
index 9111212..9e0e79d 100644
--- a/theories/PFsection8.v
+++ b/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      *)
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index 36a4ab0..9c72004 100644
--- a/theories/PFsection9.v
+++ b/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  *)
diff --git a/theories/stripped_odd_order_theorem.v b/theories/stripped_odd_order_theorem.v
index a75092f..02d79a5 100644
--- a/theories/stripped_odd_order_theorem.v
+++ b/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      *)
diff --git a/theories/wielandt_fixpoint.v b/theories/wielandt_fixpoint.v
index 21683e8..abddccb 100644
--- a/theories/wielandt_fixpoint.v
+++ b/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,     *)