incorporate new suggestions by @CohenCyril

3 files changed, 3 insertions, 3 deletions

diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 2ac2c3e..b65742d 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -2238,7 +2238,7 @@ Proof.
 apply/eqP/idP=> [d0|]; last first.
   case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|].
   by move/divp_small.
-case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| qn0].
+case: eqVneq => // _; case: eqVneq => // qn0.
 move: (divp_eq p q); rewrite d0 mul0r add0r.
 move/(f_equal (fun x : {poly R} => size x)).
 by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index dd14013..2e025a2 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -837,7 +837,7 @@ Qed.
 Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1).
 Proof.
 case: (eqsVneq G 1) => [-> |]; first by rewrite rank1.
-case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx.
+case: (trivgVpdiv G) => [/eqP->// | [p p_pr]].
 case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G).
 have EpGx: <[x]>%G \in 'E_p(G).
   by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index e4e0003..7e1cdc8 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -201,7 +201,7 @@ Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set :=
   | NeqNotEq of x != y : eq_xor_neq x y false false.
 
 Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y).
-Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed.
+Proof. by rewrite eq_sym; case: (altP eqP); constructor. Qed.
 
 Arguments eqVneq {T} x y, {T x y}.