Replace eqVneq with eqPsym

Also changed eqsVneq.

1 files changed, 5 insertions, 8 deletions

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 75a04ef..e4e0003 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,14 +196,14 @@ Proof. exact/eqP/eqP. Qed.
 
 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.
+Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set :=
+  | EqNotNeq of x = y : eq_xor_neq x y true true
+  | NeqNotEq of x != y : eq_xor_neq x y false false.
 
-Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y).
+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.
 
-Arguments eqPsym {T x y}.
+Arguments eqVneq {T} x y, {T x y}.
 
 Section Contrapositives.
 
@@ -379,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed.
 Lemma predU1r : b -> (x == y) || b.
 Proof. by move->; rewrite orbT. Qed.
 
-Lemma eqVneq : {x = y} + {x != y}.
-Proof. by case: eqP; [left | right]. Qed.
-
 End EqPred.
 
 Arguments predU1P {T x y b}.