From 37a49513f22a3f792a1ac3241962a7d17455f7e5 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 16 May 2020 09:02:13 +0900
Subject: A few more revisions

---
 mathcomp/ssreflect/generic_quotient.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

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

diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 4eeada9..5ec4037 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -482,7 +482,7 @@ Lemma equiv_sym : symmetric e. Proof. by case: e => [] ? []. Qed.
 Lemma equiv_trans : transitive e. Proof. by case: e => [] ? []. Qed.
 
 Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
-Proof. by move=> x y z; move/eqP->; move/eqP->. Qed.
+Proof. by move=> x y z /eqP -> /eqP ->. Qed.
 
 Lemma equiv_ltrans: left_transitive e.
 Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
@@ -598,8 +598,7 @@ Definition pi := locked (fun x => EquivQuotient (canon_id x)).
 
 Lemma ereprK : cancel erepr pi.
 Proof.
-unlock pi; case=> x hx; move/eqP:(hx)=> hx'.
-exact: (@val_inj _ _ [subType for erepr]).
+by unlock pi; case=> x hx; apply/(@val_inj _ _ [subType for erepr])/eqP.
 Qed.
 
 Local Notation encDE := (encModRelE encD).
@@ -629,9 +628,7 @@ exact/pi_CD.
 Qed.
 
 Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
-Proof.
-by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP.
-Qed.
+Proof. by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. Qed.
 
 Local Notation qT := (type_of (Phantom (rel D) encD)).
 Definition quotClass := QuotClass equivQTP.
-- 
cgit v1.2.3