From ed0e9311e5cab3a983f9c82a3883d955ccdb38f7 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 19 Aug 2024 13:19:42 +0200
Subject: [PATCH] adapt to MC#1256

---
 theories/abel.v                  | 4 ++--
 theories/xmathcomp/classic_ext.v | 2 +-
 theories/xmathcomp/various.v     | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/abel.v b/theories/abel.v
index e13017d..83fe7cc 100644
--- a/theories/abel.v
+++ b/theories/abel.v
@@ -650,7 +650,7 @@ Lemma solvable_ext_polyP (F : fieldType) (p : {poly F}) : p != 0 ->
                 solvable 'Gal(<<1 & rs>> / 1)).
 Proof.
 move=> p_neq0 charF; split => sol_p.
-have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1.
+have FoE (v : F^o) : v = in_alg F^o v by rewrite in_algE /(_%:A)/= mulr1.
 apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
   move=> [L [rs [iota rsf p_eq]]]; apply/classicW.
   have iotaF : iota =1 in_alg L by move=> v; rewrite [v in LHS]FoE rmorph_alg.
@@ -715,7 +715,7 @@ split => sol_p; last first.
   rewrite char0_galois// ?sub1v//.
   apply/splitting_normalField; rewrite ?sub1v//.
   by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs].
-have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1.
+have FoE (v : F^o) : v = in_alg F^o v by rewrite in_algE /(_%:A)/= mulr1.
 apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
 move=> [L [rs [f rsf p_eq]]].
 have fF : f =1 in_alg L by move=> v; rewrite [v in LHS]FoE rmorph_alg.
diff --git a/theories/xmathcomp/classic_ext.v b/theories/xmathcomp/classic_ext.v
index 168431a..e839294 100644
--- a/theories/xmathcomp/classic_ext.v
+++ b/theories/xmathcomp/classic_ext.v
@@ -119,7 +119,7 @@ rewrite eqp_monic ?monic_XnsubC ?monic_prod_XsubC// => /eqP Xnsub1E.
 have rs_uniq : uniq rs.
   rewrite -separable_prod_XsubC -Xnsub1E separable_Xn_sub_1//.
   have: in_alg L' n%:R != 0 by rewrite fmorph_eq0.
-  by rewrite raddfMn/= -(@in_algE _ L') rmorph1.
+  by rewrite raddfMn/= -in_algE rmorph1.
 have rs_ge : (n <= size rs)%N.
   have /(congr1 (fun p : {poly _} => size p)) := Xnsub1E.
   rewrite size_XnsubC// size_prod_seq; last first.
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index a064fcc..d78617e 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -776,7 +776,8 @@ do [suff init (p : {poly L}) (k : {subfield L})
       - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->.
         by rewrite -!in_algE -rmorphM => /fmorph_inj<-//; rewrite rmorphM.
       - case: sig_eqW => /= one /esym/eqP; rewrite algid1.
-        by rewrite -[X in X == _]in_algE fmorph_eq1 => /eqP->; rewrite scale1r.
+        rewrite -[X in X == _]in_algE fmorph_eq1 => /eqP->.
+        by rewrite -in_algE rmorph1.
     have fl : scalable f.
       move=> a ? /=; rewrite /f.
       case: sig_eqW => x; case: sig_eqW => /= v->.