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

src/freeg.v

@@ -27,6 +27,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype bigop order generic_quotient.
 From mathcomp Require Import ssralg ssrnum ssrint.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Import Order.Theory GRing.Theory Num.Theory.
 
@@ -38,7 +39,7 @@
 Unset Printing Implicit Defensive.
 
 (* -------------------------------------------------------------------- *)
 Local Notation simpm := Monoid.simpm.
 
 (* -------------------------------------------------------------------- *)
 Reserved Notation "{ 'freeg' K / G }" (K at level 2, format "{ 'freeg'  K  /  G }").
@@ -115,8 +116,8 @@
 
     HB.reexport.
 
     Notation prefreeg   := prefreeg.
     Notation fgequiv    := equiv.
     Notation mkPrefreeg := mkPrefreeg.
 
     Notation reduced := reduced.
@@ -569,7 +570,7 @@
   Section Lift.
     Context (M : lmodType R) (f : K -> M).
 
     Lemma lift_is_additive : additive (fglift f).
     Proof.
       elim/quotW=> [[D1 /= H1]]; elim/quotW=> [[D2 /= H2]].
       unlock fglift; rewrite ?piE [_ + _]piE /lift /=.
@@ -579,11 +580,11 @@
   End Lift.
 
   (* -------------------------------------------------------------------- *)
   Lemma coeff_is_additive x : additive (coeff x).
   Proof. exact: lift_is_additive R^o _. Qed.
 
   #[export] HB.instance Definition _ x :=
     GRing.isAdditive.Build {freeg K / R} R (coeff x)
       (coeff_is_additive x).
 
   Lemma coeff0   z   : coeff z 0 = 0               . Proof. exact: raddf0. Qed.
@@ -826,7 +827,7 @@
 
   Definition predeg (D : seq (int * K)) := \sum_(kx <- D) kx.1.
 
   Lemma deg_is_additive: additive deg.
   Proof. exact: (@lift_is_additive _ K int^o). Qed.
 
   #[export] HB.instance Definition _ :=

src/monalg.v

@@ -9,8 +9,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path choice finset fintype finfun.
 From mathcomp Require Import tuple bigop ssralg ssrint ssrnum.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Require Import xfinmap.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

src/mpoly.v

@@ -83,6 +83,7 @@ From mathcomp Require Import choice fintype tuple finfun bigop finset binomial.
 From mathcomp Require Import order fingroup perm ssralg zmodp poly ssrint.
 From mathcomp Require Import matrix vector.
 From mathcomp Require Import bigenough.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Require Import ssrcomplements freeg.
 

src/ssrcomplements.v

@@ -8,6 +8,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import choice fintype tuple finfun bigop finset order.
 From mathcomp Require Import ssralg.
+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.
@@ -180,7 +181,7 @@
 Lemma in_allpairs (S T R : eqType) (f : S -> T -> R)
   (s : seq S) (t : seq T) x y :
   injective (uncurry f) ->
   f x y \in [seq f x0 y0 | x0 <- s, y0 <- t] =
   (x \in s) && (y \in t).
 Proof.
 move=> f_inj; apply/allpairsP/andP => [|[]]; last by exists (x, y).

src/xfinmap.v

@@ -2,7 +2,8 @@
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun.
 From mathcomp Require Import choice seq path finset finfun fintype bigop.
 From mathcomp Require Import bigenough.
 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.