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/algebra/finalg.v    | 10 ++--------
 mathcomp/solvable/extremal.v |  3 ++-
 2 files changed, 4 insertions(+), 9 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index ac3a74e..9c0025b 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -125,7 +125,9 @@ Coercion countType : type >-> Countable.type.
 Canonical countType.
 Coercion finType : type >-> Finite.type.
 Canonical finType.
+Coercion baseFinGroupType : type >-> FinGroup.base_type.
 Canonical baseFinGroupType.
+Coercion finGroupType : type >-> FinGroup.type.
 Canonical finGroupType.
 Coercion zmodType : type >-> GRing.Zmodule.type.
 Canonical zmodType.
@@ -645,13 +647,9 @@ Definition countComUnitRing_finComRingType :=
   @ComRing.Pack countComUnitRingType xclass.
 Definition countComUnitRing_finUnitRingType :=
   @UnitRing.Pack countComUnitRingType xclass.
-Definition unitRing_countComRingType :=
-  @CountRing.ComRing.Pack unitRingType xclass.
 Definition unitRing_finComRingType := @ComRing.Pack unitRingType xclass.
 Definition countUnitRing_finComRingType :=
   @ComRing.Pack countUnitRingType xclass.
-Definition comRing_countUnitRingType :=
-  @CountRing.UnitRing.Pack comRingType xclass.
 Definition comRing_finUnitRingType := @UnitRing.Pack comRingType xclass.
 Definition countComRing_finUnitRingType :=
   @UnitRing.Pack countComRingType xclass.
@@ -720,10 +718,8 @@ Canonical countComUnitRing_finZmodType.
 Canonical countComUnitRing_finRingType.
 Canonical countComUnitRing_finComRingType.
 Canonical countComUnitRing_finUnitRingType.
-Canonical unitRing_countComRingType.
 Canonical unitRing_finComRingType.
 Canonical countUnitRing_finComRingType.
-Canonical comRing_countUnitRingType.
 Canonical comRing_finUnitRingType.
 Canonical countComRing_finUnitRingType.
 Canonical finComRing_finUnitRingType.
@@ -1231,7 +1227,6 @@ Definition lalg_finZmodType := @Zmodule.Pack lalgType xclass.
 Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType xclass.
 Definition lalg_countRingType := @CountRing.Ring.Pack lalgType xclass.
 Definition lalg_finRingType := @Ring.Pack lalgType xclass.
-Definition lmod_ringType := @GRing.Ring.Pack lmodType xclass.
 Definition lmod_countRingType := @CountRing.Ring.Pack lmodType xclass.
 Definition lmod_finRingType := @Ring.Pack lmodType xclass.
 Definition finLmod_ringType := @GRing.Ring.Pack finLmodType xclass.
@@ -1285,7 +1280,6 @@ Canonical lalg_finZmodType.
 Canonical lalg_finLmodType.
 Canonical lalg_countRingType.
 Canonical lalg_finRingType.
-Canonical lmod_ringType.
 Canonical lmod_countRingType.
 Canonical lmod_finRingType.
 Canonical finLmod_ringType.
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