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

src/word.v

@@ -22,11 +22,12 @@
 
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv zmodp.
 From Coq Require Import Arith ZArith Lia.
 Require Import word_ssrZ.
 
 (* -------------------------------------------------------------------- *)
+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.
@@ -470,7 +471,7 @@
 Proof. by rewrite -val_eqE. Qed.
 
 (* -------------------------------------------------------------------- *)
 HB.instance Definition _ := GRing.Zmodule_isComRing.Build n.+1.-word
   mulwA mulwC mul1w mulwDl onew_neq0.
 
 (* -------------------------------------------------------------------- *)
@@ -595,7 +596,7 @@
 Proof. by rewrite mulr_ge0 // ?exprn_ge0 // ler0n. Qed.
 
 Definition wbit (z : Z) (n : nat) : bool :=
   nosimpl (Z.testbit z (Z.of_nat n)).
 
 Lemma wbit0 i : wbit 0 i = false.
 Proof. by rewrite /wbit Z.testbit_0_l. Qed.
@@ -1004,7 +1005,7 @@
 Qed.
 
 Definition w0extend :=
   nosimpl (fun p w => mkWord (w0extend_subproof p w)).
 
 Definition wbit_w0extend (p : nat) (w : n.-word) i :
   wbit (w0extend p w) i = if i < n then wbit w i else false.
@@ -1045,9 +1046,9 @@
 + by rewrite modulusE le2Xn_sumbitsZ.
 Qed.
 
 Definition wand := nosimpl (fun w1 w2 => mkWord (wand_subproof w1 w2)).
 Definition wor  := nosimpl (fun w1 w2 => mkWord (wor_subproof  w1 w2)).
 Definition wxor := nosimpl (fun w1 w2 => mkWord (wxor_subproof w1 w2)).
 
 (* -------------------------------------------------------------------- *)
 Lemma wandE (w1 w2 : n.-word) i :

src/word_ssrZ.v

@@ -22,9 +22,10 @@
 
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv.
 From Coq Require Import Arith ZArith.
 
+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.
@@ -88,7 +89,7 @@
   Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l.
 
 (* -------------------------------------------------------------------- *)
 HB.instance Definition _ := GRing.Zmodule_isComRing.Build Z
   Z.mul_assoc Z.mul_comm Z.mul_1_l Z.mul_add_distr_r (erefl true).
 
 (* -------------------------------------------------------------------- *)
@@ -110,7 +111,7 @@
 
 End ZUnitRing.
 
 HB.instance Definition _ := GRing.ComRing_hasMulInverse.Build Z
   ZUnitRing.mulVZ ZUnitRing.unitZPl ZUnitRing.invZ_out.
 
 HB.instance Definition _ := GRing.ComUnitRing_isIntegral.Build Z