From 19ac0629d643f85ed1ec2db86f991c848ef3bbbd Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Thu, 3 Dec 2015 15:33:38 +0000
Subject: Remove spurious injections

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

(limited to 'mathcomp/odd_order/BGsection16.v')

diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v
index 3f0cf92..32850e4 100644
--- a/mathcomp/odd_order/BGsection16.v
+++ b/mathcomp/odd_order/BGsection16.v
@@ -786,7 +786,7 @@ split; first by have [_ _ _ _ []] := Ptype_structure PmaxM hallK.
 have [<- | neqMF_Ms] := eqVneq M`_\F M`_\sigma; first exact: Fcore_sub_Fitting.
 have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM).
 have [D hallD] := Hall_exists #|Kstar|^' solMs.
-by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [[->]].
+by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [->].
 Qed.
 
 End SingleGroupSummaries.
-- 
cgit v1.2.3