adapt to MC#1256

theories/abel.v

@@ -650,7 +650,7 @@
                 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 @@
   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.
@@ -902,12 +902,12 @@
 Proof.
 have := p_irr; rewrite /irreducible_poly => -[+ _].
 by apply: contraTneq => ->; rewrite size_poly0.
 Qed.
 
 Let ratr_p' : map_poly ratr p %= \prod_(x <- rp') ('X - x%:P).
 Proof.
 by have := poly_numfield_eqp p_neq0; rewrite (eq_map_poly (fmorph_eq_rat _)).
 Qed.
 
 Let rp'_uniq : uniq rp'.
 Proof.
@@ -917,7 +917,7 @@
 rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
 move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
 by case: (size p) sp_gt1 => [|[|n]]//= _; rewrite ltnn; apply.
 Qed.
 
 Let d := (size p).-1.
 Hypothesis d_prime : prime d.
@@ -926,13 +926,13 @@
 Let rp := [seq x <- rp' | iota x \isn't Num.real]
           ++ [seq x <- rp' | iota x \is Num.real].
 
 Let rp_perm : perm_eq rp rp'. Proof. by rewrite perm_catC perm_filterC. Qed.
 Let rp_uniq : uniq rp. Proof. by rewrite (perm_uniq rp_perm). Qed.
 Let ratr_p : map_poly ratr p %= \prod_(x <- rp) ('X - x%:P).
 Proof.
 rewrite (eqp_trans ratr_p')// eqp_monic ?monic_prod_XsubC//.
 exact/eqP/esym/perm_big.
 Qed.
 
 Lemma nth_rp_real i : (iota rp`_i \is Num.real) = (i > 1)%N.
 Proof.
@@ -946,16 +946,16 @@
 
 Let K := <<1 & rp'>>%AS.
 Let K_eq : K = <<1 & rp>>%AS :> {vspace _}.
 Proof. exact/esym/eq_adjoin/perm_mem. Qed.
 
 Let K_split_p : splittingFieldFor 1%AS (map_poly ratr p) K.
 Proof. by exists rp => //; rewrite ratr_p eqpxx. Qed.
 
 Let p_sep : separable_poly p.
 Proof.
 rewrite -(separable_map (char0_ratr charL)).
 by rewrite (eqp_separable ratr_p) separable_prod_XsubC.
 Qed.
 
 Let d_gt0 : (d > 0)%N.
 Proof. by rewrite prime_gt0. Qed.
@@ -1322,11 +1322,11 @@
 have p1  : Num.sg pR.[1%:~R]        = - 1 by rewrite pRE !pesimp -lock rmorphN1.
 have p2  : Num.sg pR.[2%:~R]        =   1 by rewrite pRE !pesimp -lock rmorph1.
 have simp := (pN2, pN1, p1, p2, mulN1r, mulrN1).
 have [||x0 /andP[_ x0N1] rx0] := @ivt_sign _ pR (- 2%:R) (- 1); rewrite ?simp//.
   by rewrite -subr_ge0 opprK addKr ler01.
 have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp//.
   by rewrite -subr_ge0 opprK addr_ge0 ?ler01.
 have [||x2 /andP[/= x21 _] rx2] := @ivt_sign _ pR 1 2%:R; rewrite ?simp//.
   by rewrite -subr_ge0 addrK ler01.
 have: sorted <%R [:: x0; x1; x2] by rewrite /= (lt_trans x0N1) ?(lt_trans x11).
 rewrite lt_sorted_uniq_le => /andP[uniqx012 _].

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.

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->.