From fafd4dac5315e1d4e071b0044a50a16360b31964 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 23 Nov 2017 16:33:36 +0100
Subject: running semi-automated linting on the whole library

---
 mathcomp/solvable/alt.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/solvable/alt.v')

diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index baf4792..73a3b1b 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -271,7 +271,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N.
   move: (card_Syl_dvd 5 H) (card_Syl_mod H prime_5).
   rewrite Hcard20; case: (card _) => // n Hdiv.
   move: (dvdn_leq  (isT: (0 < 20)%N) Hdiv).
-  by move: (n) Hdiv; do 20 (case => //).
+  by move: (n) Hdiv; do 20 (case=> //).
 case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS.
 have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20.
 suff: 20 %| #|S| by rewrite oS.
@@ -350,7 +350,7 @@ have Hp1: p1 x = x.
 have Hcp1: #|[set x | p1 x != x]| <= n.
   have F1 y: p y = y -> p1 y = y.
     move=> Hy; rewrite /p1 permM Hy.
-    case tpermP => //; first by move => <-.
+    case tpermP => //; first by move=> <-.
     by move=> Hpx1; apply: (@perm_inj _ p); rewrite -Hpx1.
   have F2: p1 x1 = x1 by rewrite /p1 permM tpermR.
   have F3: [set x | p1 x != x] \subset [predD1 [set x | p x != x] & x1].
-- 
cgit v1.2.3