diff --git a/examples/field_examples.v b/examples/field_examples.v
index bb31c7f..398162d 100644
--- a/examples/field_examples.v
+++ b/examples/field_examples.v
@@ -3,6 +3,7 @@
 (* Import`s below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat. *)
 (* From mathcomp.algebra_tactics Require Import ring. *)
+(* 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/examples/field_examples_check.v b/examples/field_examples_check.v
index 7b719c8..256f8f4 100644
--- a/examples/field_examples_check.v
+++ b/examples/field_examples_check.v
@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Load "field_examples.v".
diff --git a/examples/field_examples_no_check.v b/examples/field_examples_no_check.v
index 2b01d8b..7d2a1e3 100644
--- a/examples/field_examples_no_check.v
+++ b/examples/field_examples_no_check.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Ltac field_reflection ::= field_reflection_no_check.
 
diff --git a/examples/from_sander.v b/examples/from_sander.v
index b4c8b0c..4d81d5a 100644
--- a/examples/from_sander.v
+++ b/examples/from_sander.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+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/examples/lra_examples.v b/examples/lra_examples.v
index a89d2e5..42feef3 100644
--- a/examples/lra_examples.v
+++ b/examples/lra_examples.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp Require Import lra.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Local Open Scope ring_scope.
 
diff --git a/examples/ring_error.v b/examples/ring_error.v
index 176b704..f488841 100644
--- a/examples/ring_error.v
+++ b/examples/ring_error.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg.
 From mathcomp.algebra_tactics Require Import ring.
+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/examples/ring_examples.v b/examples/ring_examples.v
index 5373716..95c286b 100644
--- a/examples/ring_examples.v
+++ b/examples/ring_examples.v
@@ -2,6 +2,7 @@
 (* `ring_examples_no_check.v`. To edit this file, uncomment `Require Import`s *)
 (* below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ. *)
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 (* From mathcomp.algebra_tactics Require Import ring. *)
 
 Set Implicit Arguments.
diff --git a/examples/ring_examples_check.v b/examples/ring_examples_check.v
index 3032244..f8f8a47 100644
--- a/examples/ring_examples_check.v
+++ b/examples/ring_examples_check.v
@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From mathcomp.algebra_tactics Require Import ring.
 
 Load "ring_examples.v".
diff --git a/examples/ring_examples_no_check.v b/examples/ring_examples_no_check.v
index 7f54583..c7c0c53 100644
--- a/examples/ring_examples_no_check.v
+++ b/examples/ring_examples_no_check.v
@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From mathcomp.algebra_tactics Require Import ring.
 
 Ltac ring_reflection ::= ring_reflection_no_check.
diff --git a/theories/common.v b/theories/common.v
index 23ae533..5bfb2a6 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -7,6 +7,7 @@ From mathcomp.zify Require Import ssrZ zify.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 
+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.
 Unset Printing Implicit Defensive.
diff --git a/theories/lra.v b/theories/lra.v
index f6bb257..4642b65 100644
--- a/theories/lra.v
+++ b/theories/lra.v
@@ -8,6 +8,7 @@ From mathcomp.zify Require Import ssrZ zify.
 From mathcomp.algebra_tactics Require Import common.
 From mathcomp.algebra_tactics Extra Dependency "common.elpi" as common.
 From mathcomp.algebra_tactics Extra Dependency "lra.elpi" as lra.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Import Order.TTheory GRing.Theory Num.Theory.
 
diff --git a/theories/ring.v b/theories/ring.v
index c81192b..accb8f7 100644
--- a/theories/ring.v
+++ b/theories/ring.v
@@ -9,6 +9,7 @@ From mathcomp.algebra_tactics Extra Dependency "common.elpi" as common.
 From mathcomp.algebra_tactics Extra Dependency "ring.elpi" as ring.
 From mathcomp.algebra_tactics Extra Dependency "ring_tac.elpi" as ring_tac.
 From mathcomp.algebra_tactics Extra Dependency "field_tac.elpi" as field_tac.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Import GRing.Theory.