From e9c284b97b76e214f417ccc33907853bc0b8aa8e Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 15:37:31 +0300
Subject: incorporate new suggestions by @CohenCyril

---
 mathcomp/ssreflect/eqtype.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect')

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}.
 
-- 
cgit v1.2.3