diff --git a/theories/abel.v b/theories/abel.v
index 6c35a53..9126278 100644
--- a/theories/abel.v
+++ b/theories/abel.v
@@ -2,6 +2,7 @@ From Corelib Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various classic_ext map_gal algR.
 From Abel Require Import char0 cyclotomic_ext real_closed_ext.
 
diff --git a/theories/xmathcomp/algR.v b/theories/xmathcomp/algR.v
index 456b943..dd0ec48 100644
--- a/theories/xmathcomp/algR.v
+++ b/theories/xmathcomp/algR.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra archimedean.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various.
 
 Set Implicit Arguments.
diff --git a/theories/xmathcomp/char0.v b/theories/xmathcomp/char0.v
index 14f63bc..7d04d3f 100644
--- a/theories/xmathcomp/char0.v
+++ b/theories/xmathcomp/char0.v
@@ -1,5 +1,6 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_field.
+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/xmathcomp/classic_ext.v b/theories/xmathcomp/classic_ext.v
index 168431a..dc0b89f 100644
--- a/theories/xmathcomp/classic_ext.v
+++ b/theories/xmathcomp/classic_ext.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various cyclotomic_ext.
 
 Set Implicit Arguments.
diff --git a/theories/xmathcomp/cyclotomic_ext.v b/theories/xmathcomp/cyclotomic_ext.v
index 459c06d..43820a0 100644
--- a/theories/xmathcomp/cyclotomic_ext.v
+++ b/theories/xmathcomp/cyclotomic_ext.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import char0 various.
 
 Set Implicit Arguments.
diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v
index 29d86c4..bf60868 100644
--- a/theories/xmathcomp/map_gal.v
+++ b/theories/xmathcomp/map_gal.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various char0.
 
 Set Implicit Arguments.
diff --git a/theories/xmathcomp/mxextra.v b/theories/xmathcomp/mxextra.v
index fabd447..5163a31 100644
--- a/theories/xmathcomp/mxextra.v
+++ b/theories/xmathcomp/mxextra.v
@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.
+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/xmathcomp/real_closed_ext.v b/theories/xmathcomp/real_closed_ext.v
index f153113..dcce7bd 100644
--- a/theories/xmathcomp/real_closed_ext.v
+++ b/theories/xmathcomp/real_closed_ext.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf polyorder.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various.
 
 Set Implicit Arguments.
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index 2aa5b9c..7dcf7cf 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.
 From mathcomp Require Import all_field.
+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.