diff options
| author | Anton Trunov | 2019-05-29 15:37:31 +0300 |
|---|---|---|
| committer | Anton Trunov | 2019-05-29 15:37:31 +0300 |
| commit | e9c284b97b76e214f417ccc33907853bc0b8aa8e (patch) | |
| tree | b7a8df4adad80129e1f1ffab4308dba17816744d /mathcomp/ssreflect | |
| parent | 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 (diff) | |
incorporate new suggestions by @CohenCyril
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
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}. |