From e565f8d9bebd4fd681c34086d5448dbaebc11976 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 19 Nov 2020 18:33:21 +0100
Subject: Removing duplicate clears and turning the warning into an error

---
 mathcomp/solvable/alt.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index e67a0f9..f95069a 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -270,7 +270,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N.
   move: (dvdn_leq  (isT: (0 < 20)%N) Hdiv).
   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.
+have{} oS: #|S| = 5 by rewrite oS p_part Hcard20.
 suff: 20 %| #|S| by rewrite oS.
 apply: FF => [|S1]; last by rewrite S1 cards1 in oS.
 apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS.
-- 
cgit v1.2.3