Fixed inheritance of fieldExt / fieldOver / splitting field

3 files changed, 16 insertions, 8 deletions

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 2cf0a23..4d32364 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -359,19 +359,19 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*                           divalg_closed coerces to all the prerequisites.  *)
 (*                                                                            *)
 (*  * ComAlgebra (commutative algebra):                                       *)
-(*       comUnitAlgType R == interface type for ComAlgebra structure with     *)
+(*           comAlgType R == interface type for ComAlgebra structure with     *)
 (*                           scalars in R; R should have a comRingType        *)
 (*                           structure.                                       *)
 (*    [comAlgType R of V] == a comAlgType R structure for V created by        *)
 (*                           merging canonical algType and comRingType on V.  *)
 (*                                                                            *)
 (*  * ComUnitAlgebra (commutative algebra with computable inverses):          *)
-(*           comAlgType R == interface type for ComUnitAlgebra structure with *)
+(*       comUnitAlgType R == interface type for ComUnitAlgebra structure with *)
 (*                           scalars in R; R should have a comUnitRingType    *)
 (*                           structure.                                       *)
 (*    [comAlgType R of V] == a comAlgType R structure for V created by        *)
-(*                           merging canonical algType and                    *)
-(*                           comUnitRingType on V.                            *)
+(*                           merging canonical comAlgType and                 *)
+(*                           unitRingType on V.                               *)
 (*                                                                            *)
 (*   In addition to this structure hierarchy, we also develop a separate,     *)
 (* parallel hierarchy for morphisms linking these structures:                 *)
@@ -3305,8 +3305,6 @@ Record class_of (T : Type) : Type := Class {
   mixin : GRing.UnitRing.mixin_of (ComRing.Pack base)
 }.
 Definition base2 R m := UnitAlgebra.Class (@mixin R m).
-(* I'm not sure this base3 is needed but can't manage to get things working *)
-(* without it                                                               *)
 Definition base3 R m := ComUnitRing.Class (@mixin R m).
 Local Coercion base : class_of >-> ComAlgebra.class_of.
 Local Coercion base2 : class_of >-> UnitAlgebra.class_of.
@@ -3320,7 +3318,7 @@ Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack :=
-  fun bT b & phant_id (@Algebra.class R phR bT) (b : ComAlgebra.class_of R T) =>
+  fun bT b & phant_id (@ComAlgebra.class R phR bT) (b : ComAlgebra.class_of R T) =>
   fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m =>
   Pack (Phant R) (@Class T b m).
 
@@ -3330,7 +3328,7 @@ Definition zmodType := @Zmodule.Pack cT xclass.
 Definition ringType := @Ring.Pack cT xclass.
 Definition unitRingType := @UnitRing.Pack cT xclass.
 Definition comRingType := @ComRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass. (* Coercion base3 *)
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
 Definition lmodType := @Lmodule.Pack R phR cT xclass.
 Definition lalgType := @Lalgebra.Pack R phR cT xclass.
 Definition algType := @Algebra.Pack R phR cT xclass.
@@ -3423,6 +3421,7 @@ Proof. by rewrite exprMn exprVn. Qed.
 
 Canonical regular_comUnitRingType := [comUnitRingType of R^o].
 Canonical regular_unitAlgType := [unitAlgType R of R^o].
+Canonical regular_comUnitAlgType := [comUnitAlgType R of R^o].
 
 End ComUnitRingTheory.
 
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 3ecd00a..64239f3 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -198,6 +198,7 @@ Coercion sort : type >-> Sortclass.
 Bind Scope ring_scope with sort.
 Coercion base : class_of >-> Falgebra.class_of.
 Coercion base4 : class_of >-> Field.class_of.
+Coercion base6 : class_of >-> ComUnitAlgebra.class_of.
 Coercion eqType : type >-> Equality.type.
 Canonical eqType.
 Coercion choiceType : type >-> Choice.type.
@@ -837,6 +838,8 @@ Proof. exact: mulrCA. Qed.
 
 Canonical fieldOver_algType := AlgType K_F L_F fieldOver_scaleAr.
 Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F].
+Canonical fieldOver_comAlgType := [comAlgType K_F of L_F].
+Canonical fieldOver_comUnitAlgType := [comUnitAlgType K_F of L_F].
 
 Fact fieldOver_vectMixin : Vector.mixin_of fieldOver_lmodType.
 Proof.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 30bef47..9a2bdfd 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -370,6 +370,8 @@ Definition lmodType := @Lmodule.Pack F phF cT xclass.
 Definition lalgType := @Lalgebra.Pack F phF cT xclass.
 Definition algType := @Algebra.Pack F phF cT xclass.
 Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass.
+Definition comAlgType := @ComAlgebra.Pack F phF cT xclass.
+Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT xclass.
 Definition vectType := @Vector.Pack F phF cT xclass.
 Definition FalgType := @Falgebra.Pack F phF cT xclass.
 Definition fieldExtType := @FieldExt.Pack F phF cT xclass.
@@ -405,8 +407,12 @@ Coercion lalgType : type >-> Lalgebra.type.
 Canonical lalgType.
 Coercion algType : type >-> Algebra.type.
 Canonical algType.
+Coercion comAlgType : type >-> ComAlgebra.type.
+Canonical comAlgType.
 Coercion unitAlgType : type >-> UnitAlgebra.type.
 Canonical unitAlgType.
+Coercion comUnitAlgType : type >-> ComUnitAlgebra.type.
+Canonical comUnitAlgType.
 Coercion vectType : type >-> Vector.type.
 Canonical vectType.
 Coercion FalgType : type >-> Falgebra.type.