diff options
| author | Kazuhiko Sakaguchi | 2020-07-09 07:00:42 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-08-12 00:41:42 +0900 |
| commit | c0c2fd1e679688411c0c81ceab4066f2da5486e5 (patch) | |
| tree | c56797a13b1ffcea89318054e03956726b04bd69 | |
| parent | ea1d26eb0f0c3ada5c159dc163cdc811b5d3239d (diff) | |
Make [fieldExtType F of L] work for abstract instances
| -rw-r--r-- | mathcomp/field/fieldext.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index b8acbd6..69c1bb7 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -130,9 +130,11 @@ Definition pack := fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT : Falgebra.class_of R bT) (b : Falgebra.class_of R T) => - fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T - (@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b - Cm) b) IDm) Fm) => Pack phR (@Class T b Cm IDm Fm). + fun mT Cm IDm Fm + & phant_id (GRing.ComRing.mixin (Field.class mT)) Cm + & phant_id (GRing.IntegralDomain.mixin (Field.class mT)) IDm + & phant_id (GRing.Field.mixin (Field.class mT)) Fm => + Pack phR (@Class T b Cm IDm Fm). Definition pack_eta K := let cK := Field.class K in let Cm := ComRing.mixin cK in @@ -261,7 +263,7 @@ Canonical lmod_fieldType. Notation fieldExtType R := (type (Phant R)). Notation "[ 'fieldExtType' F 'of' L ]" := - (@pack _ (Phant F) L _ _ id _ _ _ _ id) + (@pack _ (Phant F) L _ _ id _ _ _ _ id id id) (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope. Notation "[ 'fieldExtType' F 'of' L 'for' K ]" := |