diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 330d17b63..d88d0ec27 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -17,6 +17,7 @@ From mathcomp Require normedtype sequences.
 (* The following line is for RlnE. *)
 From mathcomp Require exp.
 
+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/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
index 38e10e310..4b1afb63c 100644
--- a/analysis_stdlib/showcase/uniform_bigO.v
+++ b/analysis_stdlib/showcase/uniform_bigO.v
@@ -5,6 +5,7 @@ From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssr
 From mathcomp Require Import boolp reals Rstruct_topology ereal classical_sets.
 From mathcomp Require Import interval_inference topology normedtype landau.
 
+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/classical/cardinality.v b/classical/cardinality.v
index 48f5ed643..25669104a 100644
--- a/classical/cardinality.v
+++ b/classical/cardinality.v
@@ -38,6 +38,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 (*                                                                            *)
 (******************************************************************************)
 
+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/classical/classical_orders.v b/classical/classical_orders.v
index 4da4cba4c..cd0e5fcb4 100644
--- a/classical/classical_orders.v
+++ b/classical/classical_orders.v
@@ -18,6 +18,7 @@ From mathcomp Require Import functions set_interval.
 (*                                                                            *)
 (******************************************************************************)
 
+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/classical/classical_sets.v b/classical/classical_sets.v
index 7ab2a157c..2744c9bff 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -213,6 +213,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*                                                                            *)
 (******************************************************************************)
 
+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/classical/contra.v b/classical/contra.v
index 6692e0011..8a29abb4a 100644
--- a/classical/contra.v
+++ b/classical/contra.v
@@ -2,6 +2,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 From mathcomp Require Import boolp.
 
+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/classical/filter.v b/classical/filter.v
index 62cbb550b..a09a20979 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -169,6 +169,7 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*   variable                                                                 *)
 (******************************************************************************)
 
+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/classical/fsbigop.v b/classical/fsbigop.v
index 52ccca2ec..44064bca9 100644
--- a/classical/fsbigop.v
+++ b/classical/fsbigop.v
@@ -25,6 +25,7 @@ Reserved Notation "\sum_ ( i '\in' A ) F"
   (F at level 41, A at level 60,
     format "'[' \sum_ ( i  '\in'  A ) '/  '  F ']'").
 
+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/classical/functions.v b/classical/functions.v
index a8a65817d..63f0b2b10 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -130,6 +130,7 @@ Add Search Blacklist "_mixin_".
 (*                                                                            *)
 (******************************************************************************)
 
+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/classical/internal_Eqdep_dec.v b/classical/internal_Eqdep_dec.v
index fa30d5195..f66ed26fb 100644
--- a/classical/internal_Eqdep_dec.v
+++ b/classical/internal_Eqdep_dec.v
@@ -75,6 +75,7 @@ exact (fun Streicher_K p P x =>
 Qed.
 End Equivalences.
 
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 
 Section EqdepDec.
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 32fa8b517..0085e236d 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -15,6 +15,7 @@ From mathcomp Require Import all_ssreflect_compat finmap 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.
 Unset Printing Implicit Defensive.
diff --git a/classical/set_interval.v b/classical/set_interval.v
index b7d458cf9..a94ae2d26 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -38,6 +38,7 @@ From mathcomp Require Import functions.
 (*                                                                            *)
 (******************************************************************************)
 
+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/classical/unstable.v b/classical/unstable.v
index 2da2880f0..5da5b6b74 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -30,6 +30,7 @@ From mathcomp Require Import archimedean interval.
 Attributes warn(note="The unstable.v file should only be used inside analysis.",
   cats="internal-analysis").
 
+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/classical/wochoice.v b/classical/wochoice.v
index 9a4652a0b..722be1377 100644
--- a/classical/wochoice.v
+++ b/classical/wochoice.v
@@ -33,6 +33,7 @@ From mathcomp Require Import boolp contra.
 (*                                                                            *)
 (******************************************************************************)
 
+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/experimental_reals/distr.v b/experimental_reals/distr.v
index 3d40a0acb..3fedd2941 100644
--- a/experimental_reals/distr.v
+++ b/experimental_reals/distr.v
@@ -9,6 +9,7 @@ From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 From mathcomp Require Import realseq realsum.
 
+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/experimental_reals/realseq.v b/experimental_reals/realseq.v
index fb76cfb59..a0d551f01 100644
--- a/experimental_reals/realseq.v
+++ b/experimental_reals/realseq.v
@@ -10,6 +10,7 @@ From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 
+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/experimental_reals/realsum.v b/experimental_reals/realsum.v
index 4418622a1..b93cedb8e 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -8,6 +8,7 @@ From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
 
+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/experimental_reals/xfinmap.v b/experimental_reals/xfinmap.v
index 63f93afe3..6d4443469 100644
--- a/experimental_reals/xfinmap.v
+++ b/experimental_reals/xfinmap.v
@@ -7,6 +7,7 @@
 From mathcomp Require Import all_ssreflect_compat all_algebra.
 From mathcomp Require Export finmap.
 
+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/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 996ef3cd2..bbaa0d611 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -118,6 +118,7 @@ From mathcomp Require Import mathcomp_extra interval_inference.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v
index 855205985..2659d3371 100644
--- a/reals/prodnormedzmodule.v
+++ b/reals/prodnormedzmodule.v
@@ -11,6 +11,7 @@ From mathcomp Require Import interval_inference.
 (* The contents is likely to be moved elsewhere.                              *)
 (******************************************************************************)
 
+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/reals/real_interval.v b/reals/real_interval.v
index 97cbcf97a..d2aaa46b4 100644
--- a/reals/real_interval.v
+++ b/reals/real_interval.v
@@ -9,6 +9,7 @@ From mathcomp Require Import reals interval_inference constructive_ereal.
 (* # Sets and intervals on $\overline{\mathbb{R}}$                            *)
 (******************************************************************************)
 
+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/reals/signed.v b/reals/signed.v
index 5ea28aea9..bb793a1c6 100644
--- a/reals/signed.v
+++ b/reals/signed.v
@@ -179,6 +179,7 @@ Reserved Notation "x %:nng" (format "x %:nng").
 
 Reserved Notation "!! x" (at level 100, only parsing).
 
+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/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
index 13c675a0d..5ef445a76 100644
--- a/reals_stdlib/Rstruct.v
+++ b/reals_stdlib/Rstruct.v
@@ -39,6 +39,7 @@ the economic rights, and the successive licensors have only limited
 liability. See the COPYING file for more details.
 *)
 
+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/borel_hierarchy.v b/theories/borel_hierarchy.v
index cb6a8ea5a..943d564a3 100644
--- a/theories/borel_hierarchy.v
+++ b/theories/borel_hierarchy.v
@@ -14,6 +14,7 @@ From mathcomp Require Import measure lebesgue_measure.
 (*                                                                            *)
 (******************************************************************************)
 
+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/cantor.v b/theories/cantor.v
index 26287d1bc..6c1b71b4f 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -34,6 +34,7 @@ From mathcomp Require Import topology function_spaces.
 (*                                                                            *)
 (******************************************************************************)
 
+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/charge.v b/theories/charge.v
index c1f2626d9..6d0327c0d 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -91,6 +91,7 @@ Reserved Notation "nu .-positive_set" (at level 2, format "nu .-positive_set").
 
 Declare Scope charge_scope.
 
+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/convex.v b/theories/convex.v
index bd3856588..66a143d7e 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -33,6 +33,7 @@ From mathcomp Require Import reals topology.
 
 Reserved Notation "x <| p |> y" (format "x  <| p |>  y", at level 49).
 
+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/derive.v b/theories/derive.v
index 18a80fa3d..cd7ef1278 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -43,6 +43,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
 (*                                                                            *)
 (******************************************************************************)
 
+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/ereal.v b/theories/ereal.v
index 7953aed0a..ab7673fe8 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -50,6 +50,7 @@ From mathcomp Require Export interval_inference topology constructive_ereal.
 (*                                                                            *)
 (******************************************************************************)
 
+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/ess_sup_inf.v b/theories/ess_sup_inf.v
index 6848111cf..ba35c24d2 100644
--- a/theories/ess_sup_inf.v
+++ b/theories/ess_sup_inf.v
@@ -15,6 +15,7 @@ From mathcomp Require Import measure lebesgue_measure.
 (*                                                                            *)
 (******************************************************************************)
 
+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/esum.v b/theories/esum.v
index e1bca2c1e..970b57e3d 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -25,6 +25,7 @@ From mathcomp Require Import topology sequences normedtype numfun.
 Reserved Notation "\esum_ ( i 'in' P ) F"
   (at level 41, F at level 41, format "\esum_ ( i  'in'  P )  F").
 
+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/exp.v b/theories/exp.v
index 84e14e84a..33f7cda14 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -34,6 +34,7 @@ From mathcomp Require Import sequences derive realfun convex.
 (*                                                                            *)
 (******************************************************************************)
 
+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/ftc.v b/theories/ftc.v
index 695067a50..e72881480 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -52,6 +52,7 @@ From mathcomp Require Import derive charge.
 (*                                                                            *)
 (******************************************************************************)
 
+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/function_spaces.v b/theories/function_spaces.v
index 2c0f8294e..fe12426c5 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -108,6 +108,7 @@ Reserved Notation "{ 'compact-open' , U -> V }"
 Reserved Notation "{ 'compact-open' , F --> f }"
   (at level 0, F at level 69, format "{ 'compact-open' ,  F  -->  f }").
 
+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/gauss_integral.v b/theories/gauss_integral.v
index 317042243..1d2f6344a 100644
--- a/theories/gauss_integral.v
+++ b/theories/gauss_integral.v
@@ -12,6 +12,7 @@ From mathcomp Require Import exp trigo lebesgue_integral derive charge ftc.
 (*                                                                            *)
 (******************************************************************************)
 
+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/hoelder.v b/theories/hoelder.v
index 9f72d5a45..ea6c5d42d 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -43,6 +43,7 @@ From mathcomp Require Import lebesgue_integral numfun exp convex.
 (*                                                                            *)
 (******************************************************************************)
 
+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/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v
index c99f95e30..c52f68bf5 100644
--- a/theories/homotopy_theory/continuous_path.v
+++ b/theories/homotopy_theory/continuous_path.v
@@ -23,6 +23,7 @@ From mathcomp Require Import function_spaces wedge_sigT.
 (*                                                                            *)
 (******************************************************************************)
 
+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/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v
index 526959b7a..698ea5c6e 100644
--- a/theories/homotopy_theory/wedge_sigT.v
+++ b/theories/homotopy_theory/wedge_sigT.v
@@ -46,6 +46,7 @@ From mathcomp Require Import cardinality fsbigop reals topology function_spaces.
 (* - bipointed                                                                *)
 (******************************************************************************)
 
+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/kernel.v b/theories/kernel.v
index d5394f83b..6e066bcf6 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -75,6 +75,7 @@ From mathcomp Require Import numfun lebesgue_measure lebesgue_integral.
 (*                                                                            *)
 (******************************************************************************)
 
+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/landau.v b/theories/landau.v
index 2955f5a23..c97f7fb1c 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -97,6 +97,7 @@ From mathcomp Require Import prodnormedzmodule.
 (* transitivity, product of functions, etc.                                   *)
 (*                                                                            *)
 (******************************************************************************)
+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/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v
index 8a3a17888..99110edf3 100644
--- a/theories/lebesgue_integral_theory/giry.v
+++ b/theories/lebesgue_integral_theory/giry.v
@@ -31,6 +31,7 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral.
 
 Reserved Notation "m >>= f" (at level 49).
 
+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/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index b0c631fc1..f6bb55a80 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -27,6 +27,7 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index f609939fb..4946a51a3 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v
@@ -33,6 +33,7 @@ From mathcomp Require Import lebesgue_integral_nonneg.
 
 Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
 
+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/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
index 0725c1e7e..75158186f 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
@@ -36,6 +36,7 @@ From mathcomp Require Import realfun function_spaces simple_functions.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
index 077323a68..f1efb1606 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -46,6 +46,7 @@ From mathcomp Require Import lebesgue_Rintegral.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
index 16f8b325e..7857df2ea 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
@@ -24,6 +24,7 @@ From mathcomp Require Import lebesgue_integrable.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
index fb833273d..199f1def8 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
@@ -37,6 +37,7 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
index ab43c808c..c12faf50e 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
@@ -19,6 +19,7 @@ From mathcomp Require Import lebesgue_integral_definition.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index 1f7add944..6a49ab649 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -31,6 +31,7 @@ From mathcomp Require Import lebesgue_integral_monotone_convergence.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v
index 3d04d6b65..12f5c93df 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v
@@ -24,6 +24,7 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence.
 
 Reserved Notation "'d1 f" (at level 10, f at next level, format "''d1'  f").
 
+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/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
index 4f17ede01..5c21a1dc2 100644
--- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v
+++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
@@ -32,6 +32,7 @@ From mathcomp Require Import simple_functions.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v
index 19fd0e6a4..96573b7b5 100644
--- a/theories/lebesgue_integral_theory/simple_functions.v
+++ b/theories/lebesgue_integral_theory/simple_functions.v
@@ -60,6 +60,7 @@ Reserved Notation "{ 'sfun' aT >-> T }"
 Reserved Notation "[ 'sfun' 'of' f ]"
   (at level 0, format "[ 'sfun'  'of'  f ]").
 
+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/lebesgue_measure.v b/theories/lebesgue_measure.v
index d1e86d3bf..a74f7250b 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -39,6 +39,7 @@ From mathcomp Require Export measurable_realfun lebesgue_stieltjes_measure.
 (*                                                                            *)
 (******************************************************************************)
 
+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/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 63a700ba1..ced1df628 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -42,6 +42,7 @@ From mathcomp Require Import realfun.
 (*                                                                            *)
 (******************************************************************************)
 
+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/measurable_realfun.v b/theories/measurable_realfun.v
index b71a25b39..5c5591929 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -50,6 +50,7 @@ From mathcomp Require Export lebesgue_stieltjes_measure.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v
index 4c5e5030e..206b832b2 100644
--- a/theories/measure_theory/counting_measure.v
+++ b/theories/measure_theory/counting_measure.v
@@ -13,6 +13,7 @@ From mathcomp Require Import sequences measurable_structure measure_function.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v
index f0e99352b..6d35745c7 100644
--- a/theories/measure_theory/dirac_measure.v
+++ b/theories/measure_theory/dirac_measure.v
@@ -18,6 +18,7 @@ From mathcomp Require Import measurable_structure measure_function.
 
 Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a").
 
+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/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v
index a20242def..32f6dc978 100644
--- a/theories/measure_theory/measurable_function.v
+++ b/theories/measure_theory/measurable_function.v
@@ -24,6 +24,7 @@ Reserved Notation "{ 'mfun' aT >-> T }"
 Reserved Notation "[ 'mfun' 'of' f ]"
   (at level 0, format "[ 'mfun'  'of'  f ]").
 
+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/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v
index 5fcf19794..55ef54c1f 100644
--- a/theories/measure_theory/measurable_structure.v
+++ b/theories/measure_theory/measurable_structure.v
@@ -118,6 +118,7 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (*                                                                            *)
 (******************************************************************************)
 
+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/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v
index 2a67f58a8..b3ffcce7b 100644
--- a/theories/measure_theory/measure_extension.v
+++ b/theories/measure_theory/measure_extension.v
@@ -78,6 +78,7 @@ Reserved Notation "mu .-caratheodory" (format "mu .-caratheodory").
 Reserved Notation "mu .-cara" (format "mu .-cara").
 Reserved Notation "mu .-cara.-measurable" (format "mu .-cara.-measurable").
 
+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/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index cd339b354..1f75a83aa 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -127,6 +127,7 @@ Reserved Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }"
 Reserved Notation "{ 'finite_measure' 'set' T '->' '\bar' R }"
   (T at level 37, format "{ 'finite_measure'  'set'  T  '->'  '\bar'  R }").
 
+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/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v
index a0146ac3e..e0435b283 100644
--- a/theories/measure_theory/measure_negligible.v
+++ b/theories/measure_theory/measure_negligible.v
@@ -50,6 +50,7 @@ Reserved Notation "f = g %[ae mu ]"
 Reserved Notation "m .-null_set" (at level 2, format "m .-null_set").
 Reserved Notation "m1 `<< m2" (at level 51).
 
+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/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v
index 9dbcb5802..c4a725288 100644
--- a/theories/measure_theory/probability_measure.v
+++ b/theories/measure_theory/probability_measure.v
@@ -38,6 +38,7 @@ From mathcomp Require Import measurable_structure measure_function dirac_measure
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/normedtype_theory/complete_normed_module.v b/theories/normedtype_theory/complete_normed_module.v
index c35a24e67..cb95c2de8 100644
--- a/theories/normedtype_theory/complete_normed_module.v
+++ b/theories/normedtype_theory/complete_normed_module.v
@@ -15,6 +15,7 @@ From mathcomp Require Import normed_module.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v
index a6ba8dc4b..a8cf4c4c0 100644
--- a/theories/normedtype_theory/ereal_normedtype.v
+++ b/theories/normedtype_theory/ereal_normedtype.v
@@ -29,6 +29,7 @@ From mathcomp Require Import real_interval num_normedtype.
 (*                                                                            *)
 (******************************************************************************)
 
+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/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index 165e549d2..d4194e5d1 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -18,6 +18,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule normed_module.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 96cda52d8..0bf1ff51f 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -64,6 +64,7 @@ Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz  f").
 Reserved Notation "[ 'lipschitz' E | x 'in' A ]"
   (at level 0, x name, format "[ 'lipschitz'  E  |  x  'in'  A ]").
 
+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/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
index d2c70006e..dfeb40bbf 100644
--- a/theories/normedtype_theory/num_normedtype.v
+++ b/theories/normedtype_theory/num_normedtype.v
@@ -46,6 +46,7 @@ Reserved Notation "f @`] a , b [" (format "f  @`] a ,  b [").
 Reserved Notation "+oo_ R" (at level 3, left associativity, format "+oo_ R").
 Reserved Notation "-oo_ R" (at level 3, left associativity, format "-oo_ R").
 
+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/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 4f37fc0f8..8546e2da9 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -64,6 +64,7 @@ From mathcomp Require Import num_normedtype.
 Reserved Notation "[ 'bounded' E | x 'in' A ]"
   (at level 0, x name, format "[ 'bounded'  E  |  x  'in'  A ]").
 
+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/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v
index 94f099d4f..c1c9ef3b9 100644
--- a/theories/normedtype_theory/urysohn.v
+++ b/theories/normedtype_theory/urysohn.v
@@ -32,6 +32,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule normed_module.
 (*                                                                            *)
 (******************************************************************************)
 
+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/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v
index e7b5e27a9..286a1c02c 100644
--- a/theories/normedtype_theory/vitali_lemma.v
+++ b/theories/normedtype_theory/vitali_lemma.v
@@ -34,6 +34,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule normed_module.
 
 Reserved Notation "k *` A" (at level 40, left associativity, format "k  *`  A").
 
+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/numfun.v b/theories/numfun.v
index bc7226be3..f75aa5b76 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -43,6 +43,7 @@ Reserved Notation "{ 'nnfun' aT >-> T }"
 Reserved Notation "[ 'nnfun' 'of' f ]"
   (at level 0, format "[ 'nnfun'  'of'  f ]").
 
+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/pi_irrational.v b/theories/pi_irrational.v
index adf90c657..1ccb5494e 100644
--- a/theories/pi_irrational.v
+++ b/theories/pi_irrational.v
@@ -14,6 +14,7 @@ From mathcomp Require Import realfun lebesgue_integral derive charge ftc trigo.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v
index 64a6e04e7..b785f167a 100644
--- a/theories/probability_theory/bernoulli_distribution.v
+++ b/theories/probability_theory/bernoulli_distribution.v
@@ -21,6 +21,7 @@ From mathcomp Require Import kernel.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index 37d5579cf..e1de1f3ca 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -29,6 +29,7 @@ From mathcomp Require Import bernoulli_distribution.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v
index 46cdb0cc5..458d7ee35 100644
--- a/theories/probability_theory/binomial_distribution.v
+++ b/theories/probability_theory/binomial_distribution.v
@@ -24,6 +24,7 @@ From mathcomp Require Import bernoulli_distribution.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v
index fba1dc5fd..b09944301 100644
--- a/theories/probability_theory/exponential_distribution.v
+++ b/theories/probability_theory/exponential_distribution.v
@@ -17,6 +17,7 @@ From mathcomp Require Import lebesgue_integral ftc.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v
index d210b1628..c8dfbabb0 100644
--- a/theories/probability_theory/normal_distribution.v
+++ b/theories/probability_theory/normal_distribution.v
@@ -21,6 +21,7 @@ From mathcomp Require Import lebesgue_integral ftc gauss_integral.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v
index 206dd726f..4a4deeed6 100644
--- a/theories/probability_theory/poisson_distribution.v
+++ b/theories/probability_theory/poisson_distribution.v
@@ -16,6 +16,7 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral.
 (*                                                                            *)
 (******************************************************************************)
 
+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/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 98c8f1ad6..5f181f95a 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -59,6 +59,7 @@ Reserved Notation "'M_ P X" (at level 5, P, X at level 4, format "''M_' P  X").
 Reserved Notation "{ 'dmfun' aT >-> T }" (format "{ 'dmfun'  aT  >->  T }").
 Reserved Notation "'{' 'dRV' P >-> R '}'" (format "'{' 'dRV'  P  '>->'  R '}'").
 
+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/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v
index 304bbc90c..75486c5ea 100644
--- a/theories/probability_theory/uniform_distribution.v
+++ b/theories/probability_theory/uniform_distribution.v
@@ -18,6 +18,7 @@ From mathcomp Require Import lebesgue_integral.
 (*                                                                            *)
 (******************************************************************************)
 
+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/realfun.v b/theories/realfun.v
index b2623a30f..9fb273074 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -43,6 +43,7 @@ From mathcomp Require Import sequences real_interval numfun.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/sequences.v b/theories/sequences.v
index 3d904d757..96fd5e6b6 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -116,6 +116,7 @@ From mathcomp Require Import ereal topology tvs normedtype landau.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/showcase/pnt.v b/theories/showcase/pnt.v
index 17718529c..d0219db42 100644
--- a/theories/showcase/pnt.v
+++ b/theories/showcase/pnt.v
@@ -18,6 +18,7 @@ Import Order.POrderTheory 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/showcase/summability.v b/theories/showcase/summability.v
index e25c74799..d85a90098 100644
--- a/theories/showcase/summability.v
+++ b/theories/showcase/summability.v
@@ -10,6 +10,7 @@ From mathcomp Require Import ereal reals topology normedtype.
 (* `realsum.v`).                                                              *)
 (******************************************************************************)
 
+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/topology_theory/compact.v b/theories/topology_theory/compact.v
index 58d898e93..2d76370f1 100644
--- a/theories/topology_theory/compact.v
+++ b/theories/topology_theory/compact.v
@@ -33,6 +33,7 @@ From mathcomp Require Import uniform_structure pseudometric_structure.
 
 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/topology_theory/connected.v b/theories/topology_theory/connected.v
index 20c62edd0..089b34e00 100644
--- a/theories/topology_theory/connected.v
+++ b/theories/topology_theory/connected.v
@@ -15,6 +15,7 @@ From mathcomp Require Import topology_structure.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v
index c1c1077aa..32f974246 100644
--- a/theories/topology_theory/initial_topology.v
+++ b/theories/topology_theory/initial_topology.v
@@ -30,6 +30,7 @@ From mathcomp Require Import pseudometric_structure.
 
 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/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index b98928b60..3e530b3cd 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -22,6 +22,7 @@ From mathcomp Require Import num_topology product_topology separation_axioms.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 5be7fb319..415e7c0ee 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -15,6 +15,7 @@ From mathcomp Require Import order_topology matrix_topology.
 
 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/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v
index 200b4f9e3..47fd9820d 100644
--- a/theories/topology_theory/order_topology.v
+++ b/theories/topology_theory/order_topology.v
@@ -22,6 +22,7 @@ From mathcomp Require Import product_topology pseudometric_structure.
 
 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/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index 29afdd9c3..1e4970cc3 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -17,6 +17,7 @@ From mathcomp Require Import uniform_structure pseudometric_structure compact.
 
 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/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v
index 94eed7cc1..caeaec898 100644
--- a/theories/topology_theory/pseudometric_structure.v
+++ b/theories/topology_theory/pseudometric_structure.v
@@ -45,6 +45,7 @@ From mathcomp Require Import uniform_structure.
 
 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/topology_theory/quotient_topology.v b/theories/topology_theory/quotient_topology.v
index 2328d0d8a..3b1edd1e1 100644
--- a/theories/topology_theory/quotient_topology.v
+++ b/theories/topology_theory/quotient_topology.v
@@ -13,6 +13,7 @@ From mathcomp Require Import topology_structure.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v
index e54a5b255..10bf03e2f 100644
--- a/theories/topology_theory/separation_axioms.v
+++ b/theories/topology_theory/separation_axioms.v
@@ -53,6 +53,7 @@ From mathcomp Require Import connected supremum_topology sigT_topology.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index 5e65d45d0..8cd075fff 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -33,6 +33,7 @@ From mathcomp Require Import product_topology.
 Reserved Notation "{ 'within' A , 'continuous' f }"
   (format "{ 'within'  A ,  'continuous'  f }").
 
+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/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v
index 73ac80336..44fe76d4e 100644
--- a/theories/topology_theory/supremum_topology.v
+++ b/theories/topology_theory/supremum_topology.v
@@ -14,6 +14,7 @@ From mathcomp Require Import topology_structure uniform_structure.
 (* `sup_topology` is equipped with the `Uniform` structure                    *)
 (******************************************************************************)
 
+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/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index a8d31bc86..306a60b36 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -82,6 +82,7 @@ Reserved Notation "A °" (format "A °").
 Reserved Notation "[ 'locally' P ]" (format "[ 'locally'  P ]").
 Reserved Notation "x ^'" (format "x ^'").
 
+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/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index fb34a5602..b4162982e 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -42,6 +42,7 @@ From mathcomp Require Import topology_structure.
 (* ```                                                                        *)
 (******************************************************************************)
 
+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/trigo.v b/theories/trigo.v
index 3c9d7388b..534facc8a 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -37,6 +37,7 @@ From mathcomp Require Import measure lebesgue_measure lebesgue_integral ftc.
 (*                                                                            *)
 (******************************************************************************)
 
+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/tvs.v b/theories/tvs.v
index ce837d6f7..a22206fcd 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -53,6 +53,7 @@ From mathcomp Require Import topology function_spaces.
 (* - The product of two Tvs is endowed with the structure of Tvs.             *)
 (******************************************************************************)
 
+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.