diff options
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 839efa7..21394bd 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -113,10 +113,12 @@ Definition axiom_def n (V : lmodType R) of phant V := Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V). -Structure class_of V := Class { +Set Primitive Projections. +Record class_of V := Class { base : GRing.Lmodule.class_of R V; mixin : mixin_of (GRing.Lmodule.Pack _ base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Lmodule.class_of. Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. @@ -124,18 +126,16 @@ Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). Definition class := let: Pack _ c := cT return class_of cT in c. Definition clone c of phant_id class c := @Pack phR T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition dim := let: Mixin n _ := mixin class in n. Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) := fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b => fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition zmodType := @GRing.Zmodule.Pack cT xclass. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. End ClassDef. Notation axiom n V := (axiom_def n (Phant V)). |