From 35bd8708dacfb508f896d957d7b1189ca7decb3e Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 13 May 2020 13:11:14 +0900
Subject: Revise proofs in ssreflect/*.v

This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
---
 mathcomp/ssreflect/eqtype.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/eqtype.v')

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 12b0601..bd58e01 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -409,7 +409,7 @@ Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y).
 Proof. by move/bij_inj; apply: inj_eq. Qed.
 
 Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y).
-Proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply: can_eq. Qed.
+Proof. by move=> fK gK x y; rewrite -[y in LHS]gK; apply: can_eq. Qed.
 
 Lemma inj_in_eq :
   {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}.
-- 
cgit v1.2.3