From 1aa27b589c437b88cc6fb556edfceac42da449ea Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 12:52:42 +0300
Subject: Canonical way of expressing dis-equality on an eqType is x != y

Addressing a suggestion by @CohenCyril
---
 mathcomp/ssreflect/eqtype.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 1f700fa..75a04ef 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -198,10 +198,10 @@ Hint Resolve eq_refl eq_sym : core.
 
 Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set :=
   | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true
-  | NeqNotEqSym of x <> y : eq_xor_neq_sym x y false false.
+  | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false.
 
 Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y).
-Proof. by rewrite eq_sym; case: eqP; constructor. Qed.
+Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed.
 
 Arguments eqPsym {T x y}.
 
-- 
cgit v1.2.3