Merge pull request #248 from anton-trunov/remove-Type-from-packed-classes

Remove `_ : Type` from packed classes

1 files changed, 11 insertions, 11 deletions

diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 542f8ad..75b2073 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -117,27 +117,27 @@ Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
 
 Structure class_of V := Class {
   base : GRing.Lmodule.class_of R V;
-  mixin : mixin_of (GRing.Lmodule.Pack _ base V)
+  mixin : mixin_of (GRing.Lmodule.Pack _ base)
 }.
 Local Coercion base : class_of >-> GRing.Lmodule.class_of.
 
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
 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 T.
-Let xT := let: Pack T _ _ := cT in T.
+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 T)) :=
+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) T.
+  fun    m & phant_id m0 m => Pack phR (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+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.
 
 End ClassDef.
 Notation axiom n V := (axiom_def n (Phant V)).