From da783dd87aa95c04e038c64231908a397a44f568 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 26 Feb 2026 13:06:20 +0100
Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1545

---
 src/freeg.v          | 1 +
 src/monalg.v         | 1 +
 src/mpoly.v          | 1 +
 src/ssrcomplements.v | 1 +
 src/xfinmap.v        | 1 +
 5 files changed, 5 insertions(+)

diff --git a/src/freeg.v b/src/freeg.v
index a116fe7..fd0bcfd 100644
--- a/src/freeg.v
+++ b/src/freeg.v
@@ -27,6 +27,7 @@ From HB Require Import structures.
 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.
 
diff --git a/src/monalg.v b/src/monalg.v
index 5ed67e6..6c90b3c 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -9,6 +9,7 @@ From HB Require Import structures.
 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.
 
diff --git a/src/mpoly.v b/src/mpoly.v
index 75f2e3a..b514e39 100644
--- a/src/mpoly.v
+++ b/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.
 
diff --git a/src/ssrcomplements.v b/src/ssrcomplements.v
index 7b1c24a..6401c20 100644
--- a/src/ssrcomplements.v
+++ b/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.
diff --git a/src/xfinmap.v b/src/xfinmap.v
index 216b80b..b975251 100644
--- a/src/xfinmap.v
+++ b/src/xfinmap.v
@@ -3,6 +3,7 @@ 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.