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

theories/abel.v

@@ -2,6 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various classic_ext map_gal algR.
 From Abel Require Import char0 cyclotomic_ext real_closed_ext.
 
@@ -903,12 +904,12 @@
 Proof.
 have := p_irr; rewrite /irreducible_poly => -[+ _].
 by apply: contraTneq => ->; rewrite size_poly0.
 Qed.
 
 Let ratr_p' : map_poly ratr p %= \prod_(x <- rp') ('X - x%:P).
 Proof.
 by have := poly_numfield_eqp p_neq0; rewrite (eq_map_poly (fmorph_eq_rat _)).
 Qed.
 
 Let rp'_uniq : uniq rp'.
 Proof.
@@ -918,7 +919,7 @@
 rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
 move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
 by case: (size p) sp_gt1 => [|[|n]]//= _; rewrite ltnn; apply.
 Qed.
 
 Let d := (size p).-1.
 Hypothesis d_prime : prime d.
@@ -927,13 +928,13 @@
 Let rp := [seq x <- rp' | iota x \isn't Num.real]
           ++ [seq x <- rp' | iota x \is Num.real].
 
 Let rp_perm : perm_eq rp rp'. Proof. by rewrite perm_catC perm_filterC. Qed.
 Let rp_uniq : uniq rp. Proof. by rewrite (perm_uniq rp_perm). Qed.
 Let ratr_p : map_poly ratr p %= \prod_(x <- rp) ('X - x%:P).
 Proof.
 rewrite (eqp_trans ratr_p')// eqp_monic ?monic_prod_XsubC//.
 exact/eqP/esym/perm_big.
 Qed.
 
 Lemma nth_rp_real i : (iota rp`_i \is Num.real) = (i > 1)%N.
 Proof.
@@ -947,16 +948,16 @@
 
 Let K := <<1 & rp'>>%AS.
 Let K_eq : K = <<1 & rp>>%AS :> {vspace _}.
 Proof. exact/esym/eq_adjoin/perm_mem. Qed.
 
 Let K_split_p : splittingFieldFor 1%AS (map_poly ratr p) K.
 Proof. by exists rp => //; rewrite ratr_p eqpxx. Qed.
 
 Let p_sep : separable_poly p.
 Proof.
 rewrite -(separable_map (char0_ratr charL)).
 by rewrite (eqp_separable ratr_p) separable_prod_XsubC.
 Qed.
 
 Let d_gt0 : (d > 0)%N.
 Proof. by rewrite prime_gt0. Qed.
@@ -1323,11 +1324,11 @@
 have p1  : Num.sg pR.[1%:~R]        = - 1 by rewrite pRE !pesimp -lock rmorphN1.
 have p2  : Num.sg pR.[2%:~R]        =   1 by rewrite pRE !pesimp -lock rmorph1.
 have simp := (pN2, pN1, p1, p2, mulN1r, mulrN1).
 have [||x0 /andP[_ x0N1] rx0] := @ivt_sign _ pR (- 2%:R) (- 1); rewrite ?simp//.
   by rewrite -subr_ge0 opprK addKr ler01.
 have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp//.
   by rewrite -subr_ge0 opprK addr_ge0 ?ler01.
 have [||x2 /andP[/= x21 _] rx2] := @ivt_sign _ pR 1 2%:R; rewrite ?simp//.
   by rewrite -subr_ge0 addrK ler01.
 have: sorted <%R [:: x0; x1; x2] by rewrite /= (lt_trans x0N1) ?(lt_trans x11).
 rewrite lt_sorted_uniq_le => /andP[uniqx012 _].

theories/xmathcomp/algR.v

@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra archimedean.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various.
 
 Set Implicit Arguments.

theories/xmathcomp/char0.v

@@ -1,5 +1,6 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/xmathcomp/classic_ext.v

@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various cyclotomic_ext.
 
 Set Implicit Arguments.

theories/xmathcomp/cyclotomic_ext.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import char0 various.
 
 Set Implicit Arguments.

theories/xmathcomp/map_gal.v

@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various char0.
 
 Set Implicit Arguments.

theories/xmathcomp/mxextra.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/xmathcomp/real_closed_ext.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf polyorder.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From Abel Require Import various.
 
 Set Implicit Arguments.
@@ -39,7 +40,7 @@
 have peq0 i : (i < n)%N -> p.[s`_i] = 0.
   by move=> i_lt; apply/rootP; rewrite -[root _ _]mem_rootsR// mem_nth.
 have peq (i : 'I_n.-1) : p.[s`_i] = p.[s`_(i.+1)] by rewrite !peq0// ltnW.
 have /all_sig2[r rs p'r] := rolle (slt _) (peq _).
 have rtE (i : 'I_n.-1) : [tuple r i | i < n.-1]`_i = r i.
   by rewrite (nth_map i) ?size_enum_ord ?nth_ord_enum.
 suff /(sorted_uniq lt_trans lt_irreflexive) : sorted <%R [tuple r i | i < _].

theories/xmathcomp/various.v

@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.
 From mathcomp Require Import all_field.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.