Adapt to https://github.com/math-comp/math-comp/pull/1545

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.