From 407b4c412d4a1324450d01fa09a41aad7673b1bf Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 5 Apr 2019 19:09:06 +0200
Subject: Fix inheritance bugs in finalg and extremal

---
 mathcomp/solvable/extremal.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp/solvable')

diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 9ac5236..a51fe9c 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -1533,7 +1533,8 @@ Canonical extremal_group_countType := CountType _ extremal_group_countMixin.
 Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
 Proof. by case: c. Qed.
 Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups.
-Canonical extremal_group_finType := FinType _ extremal_group_finMixin.
+Canonical extremal_group_finType :=
+  FinType extremal_group_type extremal_group_finMixin.
 
 Definition extremal_class (A : {set gT}) :=
   let m := #|A| in let p := pdiv m in let n := logn p m in
-- 
cgit v1.2.3