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

examples/field_examples.v

@@ -3,6 +3,7 @@
 (* Import`s below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat. *)
 (* From mathcomp.algebra_tactics Require Import ring. *)
+(* 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.

examples/field_examples_check.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Load "field_examples.v".

examples/field_examples_no_check.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Ltac field_reflection ::= field_reflection_no_check.
 

examples/from_sander.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.algebra_tactics Require Import ring.
+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.

examples/lra_examples.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp Require Import lra.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Local Open Scope ring_scope.
 

examples/ring_error.v

@@ -1,5 +1,6 @@
 From mathcomp Require Import all_ssreflect ssralg.
 From mathcomp.algebra_tactics Require Import ring.
+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.

examples/ring_examples.v

@@ -2,6 +2,7 @@
 (* `ring_examples_no_check.v`. To edit this file, uncomment `Require Import`s *)
 (* below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ. *)
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 (* From mathcomp.algebra_tactics Require Import ring. *)
 
 Set Implicit Arguments.

examples/ring_examples_check.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From mathcomp.algebra_tactics Require Import ring.
 
 Load "ring_examples.v".

examples/ring_examples_no_check.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From mathcomp.algebra_tactics Require Import ring.
 
 Ltac ring_reflection ::= ring_reflection_no_check.

theories/common.v

@@ -1,12 +1,13 @@
 From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import PeanoNat BinNat Zbool QArith.
 From Coq.micromega Require Import OrderedRing RingMicromega.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp.zify Require Import ssrZ zify.
 
 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.
@@ -384,9 +385,9 @@
 
 Variables (R' : pzSemiRingType).
 
 Notation Rnorm :=
   (Rnorm (fun n => (nat_of_N n)%:R) 0 +%R 1 *%R (fun x n => x ^+ N.to_nat n)).
 Notation Mnorm :=
   (Mnorm (fun n => (nat_of_N n)%:R) 0 +%R 1 *%R (fun x n => x ^+ N.to_nat n)).
 
 Lemma Rnorm_correct_rec R (f : {rmorphism R -> R'}) (e : RExpr R) :
@@ -554,10 +555,10 @@
 
 Variables (R' : pzRingType).
 
 Notation Rnorm :=
   (Rnorm (fun n : Z => (int_of_Z n)%:~R) 0 +%R -%R (fun x y => x - y)
      1 *%R (fun x n => x ^+ N.to_nat n)).
 Notation Mnorm :=
   (Mnorm (fun n : Z => (int_of_Z n)%:~R) 0 +%R -%R (fun x y => x - y)
      1 *%R (fun x n => x ^+ N.to_nat n)).
 
@@ -758,10 +759,10 @@
 
 Variables (F : fieldType).
 
 Notation Rnorm :=
   (Rnorm (fun (n : Z) => (int_of_Z n)%:~R) 0 +%R -%R (fun x y => x - y)
      1 *%R (fun x n => x ^+ N.to_nat n) GRing.inv).
 Notation Mnorm :=
   (Mnorm (fun (n : Z) => (int_of_Z n)%:~R) 0 +%R -%R (fun x y => x - y)
      1 *%R (fun x n => x ^+ N.to_nat n) GRing.inv).
 
@@ -1069,7 +1070,7 @@
 
 Variables (F : fieldType).
 
 Notation F_of_Z :=
   (fun b (n : Z) => if b then (int_of_Z n)%:~R^-1 else (int_of_Z n)%:~R).
 Notation Rnorm :=
   (Rnorm F_of_Z 0 +%R -%R (fun x y => x - y)
@@ -1332,7 +1333,7 @@
 Proof.
 rewrite /Qeq_bool /R_of_Q /= eqr_div ?pnatr_eq0; try lia.
 rewrite !pmulrn -!intrM eqr_int -!/(int_of_Z (Z.pos _)) -!rmorphM /=.
 by rewrite (can_eq int_of_ZK); apply/idP/eqP => /Zeq_is_eq_bool.
 Qed.
 
 Lemma R_of_Q_le x y : Qle_bool x y = (R_of_Q x <= R_of_Q y :> F).

theories/lra.v

@@ -1,6 +1,6 @@
 From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import BinNat QArith Ring.
 From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto Lqa.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
@@ -8,6 +8,7 @@
 From mathcomp.algebra_tactics Require Import common.
 From mathcomp.algebra_tactics Extra Dependency "common.elpi" as common.
 From mathcomp.algebra_tactics Extra Dependency "lra.elpi" as lra.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Import Order.TTheory GRing.Theory Num.Theory.
 

theories/ring.v

@@ -1,6 +1,6 @@
 From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import ZArith Ring Ring_polynom Field_theory.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
 From mathcomp.zify Require Import ssrZ zify.
@@ -9,6 +9,7 @@
 From mathcomp.algebra_tactics Extra Dependency "ring.elpi" as ring.
 From mathcomp.algebra_tactics Extra Dependency "ring_tac.elpi" as ring_tac.
 From mathcomp.algebra_tactics Extra Dependency "field_tac.elpi" as field_tac.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Import GRing.Theory.