From a06d61a8e226eeabc52f1a22e469dca1e6077065 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 29 Nov 2019 01:19:33 +0900
Subject: Refactoring and linting especially polydiv

- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
  The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
  introduces a hypothesis in the form of `x != y` in the second case. Thus,
  `case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
  can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
  `case: (eqVneq x y)` respectively. This replacement slightly simplifies and
  reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.
---
 mathcomp/ssreflect/path.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index d9ab11c..2790aa8 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -368,7 +368,7 @@ Proof.
 elim: s => [| h s]; first by case: ifP.
 rewrite mem2_cons => ->.
 do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=.
-by case: eqVneq => [->|]; case: eqVneq.
+by have [->|] := eqVneq; case: eqVneq.
 Qed.
 
 Variant split2r x y : seq T -> Type :=
@@ -916,7 +916,7 @@ Let le_lex_transitive x sT : transitive (le_lex x sT).
 Proof.
 move=> ? ? ? /andP [xy /implyP xy'] /andP [yz /implyP yz'].
 rewrite /= (leT_tr xy yz) /=; apply/implyP => zx.
-by apply/ltn_trans: (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)).
+exact: ltn_trans (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)).
 Qed.
 
 Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s).
-- 
cgit v1.2.3