diff --git a/theories/numbers/ssetc.v b/theories/numbers/ssetc.v
index b5a738f..6ca10cc 100644
--- a/theories/numbers/ssetc.v
+++ b/theories/numbers/ssetc.v
@@ -5,6 +5,7 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat order.
 From mathcomp Require Import ssralg ssrnum ssrint div.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export ssetz ssetq1 ssetq2 ssetr.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssete11.v b/theories/numbers/ssete11.v
index dcb9cab..3b3fdfd 100644
--- a/theories/numbers/ssete11.v
+++ b/theories/numbers/ssete11.v
@@ -3,6 +3,7 @@
 *)
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrfun.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete2 ssetq1.
 
 (* $Id: ssete11.v,v 1.8 2018/09/04 07:58:00 grimm Exp $ *)
diff --git a/theories/numbers/ssete6.v b/theories/numbers/ssete6.v
index a6255f8..dee6624 100644
--- a/theories/numbers/ssete6.v
+++ b/theories/numbers/ssete6.v
@@ -5,6 +5,7 @@ $Id: ssete6.v,v 1.31 2018/10/01 14:40:54 grimm Exp $
 *)
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 ssete2 ssete3 ssetq2.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssete7.v b/theories/numbers/ssete7.v
index 1b0823a..33e89a6 100644
--- a/theories/numbers/ssete7.v
+++ b/theories/numbers/ssete7.v
@@ -6,6 +6,7 @@ From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import ssrnat seq path div.
 From mathcomp Require Import fintype tuple finfun bigop finset binomial.
+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/numbers/ssete8.v b/theories/numbers/ssete8.v
index 540cdb4..0a61e0e 100644
--- a/theories/numbers/ssete8.v
+++ b/theories/numbers/ssete8.v
@@ -6,6 +6,7 @@ $Id: ssete8.v,v 1.2 2018/07/13 12:58:25 grimm Exp $
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import ssrnat seq choice fintype binomial.
 From mathcomp Require Import bigop ssralg poly ssrint.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Import ssete7.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssetq1.v b/theories/numbers/ssetq1.v
index 00023b2..b78d1b8 100644
--- a/theories/numbers/ssetq1.v
+++ b/theories/numbers/ssetq1.v
@@ -4,6 +4,7 @@
 (* $Id: ssetq1.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetz.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssetq2.v b/theories/numbers/ssetq2.v
index c99433f..ebc6ad6 100644
--- a/theories/numbers/ssetq2.v
+++ b/theories/numbers/ssetq2.v
@@ -4,6 +4,7 @@
 (* $Id: ssetq2.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetq1.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssetr.v b/theories/numbers/ssetr.v
index ddd4830..8ebb5c7 100644
--- a/theories/numbers/ssetr.v
+++ b/theories/numbers/ssetr.v
@@ -4,6 +4,7 @@
 (* $Id: ssetr.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetq2.
 
 Set Implicit Arguments.
diff --git a/theories/numbers/ssetz.v b/theories/numbers/ssetz.v
index 610efb6..d08c94c 100644
--- a/theories/numbers/ssetz.v
+++ b/theories/numbers/ssetz.v
@@ -5,6 +5,7 @@
 (* $Id: ssetz.v,v 1.7 2018/10/01 14:40:54 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset11.v b/theories/ordinals/sset11.v
index b80dab7..df44892 100644
--- a/theories/ordinals/sset11.v
+++ b/theories/ordinals/sset11.v
@@ -4,6 +4,7 @@
 (* $Id: sset11.v,v 1.6 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset12.v b/theories/ordinals/sset12.v
index 21d6e0e..5de3095 100644
--- a/theories/ordinals/sset12.v
+++ b/theories/ordinals/sset12.v
@@ -4,6 +4,7 @@
 (* $Id: sset12.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset11.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset13a.v b/theories/ordinals/sset13a.v
index 76c7712..f41f254 100644
--- a/theories/ordinals/sset13a.v
+++ b/theories/ordinals/sset13a.v
@@ -5,6 +5,7 @@
 (* $Id: sset13a.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset12.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset13b.v b/theories/ordinals/sset13b.v
index 7bb0c96..e277a62 100644
--- a/theories/ordinals/sset13b.v
+++ b/theories/ordinals/sset13b.v
@@ -5,6 +5,7 @@
 (* $Id: sset13b.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13a.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset13c.v b/theories/ordinals/sset13c.v
index 367a066..ae8e6ea 100644
--- a/theories/ordinals/sset13c.v
+++ b/theories/ordinals/sset13c.v
@@ -5,6 +5,7 @@
 (* $Id: sset13c.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset14.v b/theories/ordinals/sset14.v
index d69c5bc..7ee0f9f 100644
--- a/theories/ordinals/sset14.v
+++ b/theories/ordinals/sset14.v
@@ -5,6 +5,7 @@
 (* $Id: sset14.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset15.v b/theories/ordinals/sset15.v
index 10df3f5..00a6963 100644
--- a/theories/ordinals/sset15.v
+++ b/theories/ordinals/sset15.v
@@ -5,6 +5,7 @@
 (* $Id: sset15.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. 
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13c sset14.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset16a.v b/theories/ordinals/sset16a.v
index 7868af6..71e11c3 100644
--- a/theories/ordinals/sset16a.v
+++ b/theories/ordinals/sset16a.v
@@ -6,6 +6,7 @@
 
 From Coq Require Import BinNat.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div.
+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/ordinals/sset16b.v b/theories/ordinals/sset16b.v
index aeed119..f304128 100644
--- a/theories/ordinals/sset16b.v
+++ b/theories/ordinals/sset16b.v
@@ -5,6 +5,7 @@
 (* $Id: sset16b.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 sset16a. 
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset16c.v b/theories/ordinals/sset16c.v
index a375cef..a1b338c 100644
--- a/theories/ordinals/sset16c.v
+++ b/theories/ordinals/sset16c.v
@@ -5,6 +5,7 @@
 (* $Id: sset16c.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/sset17.v b/theories/ordinals/sset17.v
index a684e9c..a09f546 100644
--- a/theories/ordinals/sset17.v
+++ b/theories/ordinals/sset17.v
@@ -5,6 +5,7 @@
 (* $Id: sset17.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/ssete10.v b/theories/ordinals/ssete10.v
index 8f2a577..17f4a04 100644
--- a/theories/ordinals/ssete10.v
+++ b/theories/ordinals/ssete10.v
@@ -4,6 +4,7 @@
 (* $Id: ssete10.v,v 1.3 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete9.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/ssete2.v b/theories/ordinals/ssete2.v
index bf885b4..300be01 100644
--- a/theories/ordinals/ssete2.v
+++ b/theories/ordinals/ssete2.v
@@ -4,6 +4,7 @@
 (* $Id: ssete2.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b ssete1.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/ssete3.v b/theories/ordinals/ssete3.v
index 7cc769a..64acfb4 100644
--- a/theories/ordinals/ssete3.v
+++ b/theories/ordinals/ssete3.v
@@ -4,6 +4,7 @@
 (* $Id: ssete3.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete1 ssete2.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/ssete4.v b/theories/ordinals/ssete4.v
index a733e95..9af45ef 100644
--- a/theories/ordinals/ssete4.v
+++ b/theories/ordinals/ssete4.v
@@ -4,6 +4,7 @@
 (* $Id: ssete4.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.  
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export ssete3.
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/ssete5.v b/theories/ordinals/ssete5.v
index 7d89ee5..d9d3570 100644
--- a/theories/ordinals/ssete5.v
+++ b/theories/ordinals/ssete5.v
@@ -4,6 +4,7 @@
 (* $Id: ssete5.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 ssete4.
 
 Set Implicit Arguments.
diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v
index 82029c1..30292e1 100644
--- a/theories/schutte/ssete9.v
+++ b/theories/schutte/ssete9.v
@@ -5,6 +5,7 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import fintype bigop.
+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/sets/sset1.v b/theories/sets/sset1.v
index ea12f2f..394e232 100644
--- a/theories/sets/sset1.v
+++ b/theories/sets/sset1.v
@@ -5,6 +5,7 @@ Copyright INRIA (2009-2013 2018) Apics-Marelle Team (Jose Grimm).
 *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+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/sets/sset10.v b/theories/sets/sset10.v
index 43e73c4..2868204 100644
--- a/theories/sets/sset10.v
+++ b/theories/sets/sset10.v
@@ -5,6 +5,7 @@
 (* $Id: sset10.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset9.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset18.v b/theories/sets/sset18.v
index d276b03..afd5474 100644
--- a/theories/sets/sset18.v
+++ b/theories/sets/sset18.v
@@ -5,6 +5,7 @@
 (* $Id: sset18.v,v 1.8 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset19.v b/theories/sets/sset19.v
index d1e9282..14a3d14 100644
--- a/theories/sets/sset19.v
+++ b/theories/sets/sset19.v
@@ -5,6 +5,7 @@
 (* $Id: sset19.v,v 1.7 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset2.v b/theories/sets/sset2.v
index 9a9afa0..079f0d4 100644
--- a/theories/sets/sset2.v
+++ b/theories/sets/sset2.v
@@ -6,6 +6,7 @@
 
 From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset1.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset2_aux.v b/theories/sets/sset2_aux.v
index b3017c5..cd29ae1 100644
--- a/theories/sets/sset2_aux.v
+++ b/theories/sets/sset2_aux.v
@@ -5,6 +5,7 @@
 (* $Id: sset2_aux.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset1 sset3.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset3.v b/theories/sets/sset3.v
index fcbc654..4f1b3b7 100644
--- a/theories/sets/sset3.v
+++ b/theories/sets/sset3.v
@@ -3,6 +3,7 @@
 *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset2.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset4.v b/theories/sets/sset4.v
index 31f6444..e2b89ff 100644
--- a/theories/sets/sset4.v
+++ b/theories/sets/sset4.v
@@ -5,6 +5,7 @@
 (* $Id: sset4.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset3.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset5.v b/theories/sets/sset5.v
index a46ae18..3dd3591 100644
--- a/theories/sets/sset5.v
+++ b/theories/sets/sset5.v
@@ -5,6 +5,7 @@
 (* $Id: sset5.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset4.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset6.v b/theories/sets/sset6.v
index f59a14c..1201c30 100644
--- a/theories/sets/sset6.v
+++ b/theories/sets/sset6.v
@@ -4,6 +4,7 @@ Copyright INRIA (2009-2013 2018) Apics, Marelle Team (Jose Grimm).  *)
 (* $Id: sset6.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. 
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset5.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset7.v b/theories/sets/sset7.v
index cb9ad16..60b7079 100644
--- a/theories/sets/sset7.v
+++ b/theories/sets/sset7.v
@@ -5,6 +5,7 @@
 (* $Id: sset7.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset6.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset8.v b/theories/sets/sset8.v
index 5b86451..d7a08a7 100644
--- a/theories/sets/sset8.v
+++ b/theories/sets/sset8.v
@@ -5,6 +5,7 @@
 (* $Id: sset8.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset7.
 
 Set Implicit Arguments.
diff --git a/theories/sets/sset9.v b/theories/sets/sset9.v
index cc5eaf6..a28f32a 100644
--- a/theories/sets/sset9.v
+++ b/theories/sets/sset9.v
@@ -5,6 +5,7 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import binomial div.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset8.
 
 Set Implicit Arguments.
diff --git a/theories/sets/ssete1.v b/theories/sets/ssete1.v
index a8808a6..0cf777f 100644
--- a/theories/sets/ssete1.v
+++ b/theories/sets/ssete1.v
@@ -4,6 +4,7 @@
 (* $Id: ssete1.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset4.
 
 Set Implicit Arguments.
diff --git a/theories/stern/fibm.v b/theories/stern/fibm.v
index 4b64fca..3a7042b 100644
--- a/theories/stern/fibm.v
+++ b/theories/stern/fibm.v
@@ -7,6 +7,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path fintype div bigop binomial.
 From mathcomp Require Import prime finset ssralg ssrnum ssrint.
+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/stern/stern.v b/theories/stern/stern.v
index 577c946..b12b6aa 100644
--- a/theories/stern/stern.v
+++ b/theories/stern/stern.v
@@ -9,6 +9,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq choice fintype order bigop ssralg.
 From mathcomp Require Import div ssrnum ssrint rat prime path binomial.
 From mathcomp Require Import tuple finset.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Import fibm.
 
 Set Implicit Arguments.