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

Remove `_ : Type` from packed classes

6 files changed, 776 insertions, 771 deletions

diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v
index 21000e4..f82a231 100644
--- a/mathcomp/algebra/countalg.v
+++ b/mathcomp/algebra/countalg.v
@@ -44,14 +44,14 @@ Variables (type base_type : Type) (class_of base_of : Type -> Type).
 Variable base_sort : base_type -> Type.
 
 (* Explicits *)
-Variable Pack : forall T, class_of T -> Type -> type.
+Variable Pack : forall T, class_of T -> type.
 Variable Class : forall T, base_of T -> mixin_of T -> class_of T.
 Variable base_class : forall bT, base_of (base_sort bT).
 
 Definition gen_pack T :=
   fun bT b & phant_id (base_class bT) b =>
   fun fT c m & phant_id (Countable.class fT) (Countable.Class c m) =>
-  Pack (@Class T b m) T.
+  Pack (@Class T b m).
 
 End Generic.
 
@@ -69,20 +69,20 @@ Record class_of M :=
 Local Coercion base : class_of >-> GRing.Zmodule.class_of.
 Local Coercion mixin : class_of >-> mixin_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Zmodule.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
 
-Definition join_countType := @Countable.Pack zmodType (cnt_ xclass) xT.
+Definition join_countType := @Countable.Pack zmodType (cnt_ xclass).
 
 End ClassDef.
 
@@ -117,22 +117,22 @@ Definition base2 R (c : class_of R) := Zmodule.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.Ring.class_of.
 Local Coercion base2 : class_of >-> Zmodule.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Ring.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass cT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition join_countType := @Countable.Pack ringType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack ringType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition join_countType := @Countable.Pack ringType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack ringType xclass.
 
 End ClassDef.
 
@@ -173,25 +173,25 @@ Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.ComRing.class_of.
 Local Coercion base2 : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.ComRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition join_countType := @Countable.Pack comRingType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack comRingType xclass xT.
-Definition join_countRingType := @Ring.Pack comRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition join_countType := @Countable.Pack comRingType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack comRingType xclass.
+Definition join_countRingType := @Ring.Pack comRingType xclass.
 
 End ClassDef.
 
@@ -237,26 +237,26 @@ Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.UnitRing.class_of.
 Local Coercion base2 : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.UnitRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
 
-Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack unitRingType xclass xT.
-Definition join_countRingType := @Ring.Pack unitRingType xclass xT.
+Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack unitRingType xclass.
+Definition join_countRingType := @Ring.Pack unitRingType xclass.
 
 End ClassDef.
 
@@ -304,36 +304,36 @@ Local Coercion base : class_of >-> GRing.ComUnitRing.class_of.
 Local Coercion base2 : class_of >-> ComRing.class_of.
 Local Coercion base3 : class_of >-> UnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.ComUnitRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition countComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-
-Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass xT.
-Definition join_countRingType := @Ring.Pack comUnitRingType xclass xT.
-Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass xT.
-Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass xT.
-Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass xT.
-Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition countComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition countUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+
+Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass.
+Definition join_countRingType := @Ring.Pack comUnitRingType xclass.
+Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass.
+Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass.
+Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass.
+Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass.
 Definition ccjoin_countUnitRingType :=
-  @UnitRing.Pack countComRingType xclass xT.
+  @UnitRing.Pack countComRingType xclass.
 
 End ClassDef.
 
@@ -393,35 +393,35 @@ Definition base2 R (c : class_of R) := ComUnitRing.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
 Local Coercion base2 : class_of >-> ComUnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition countComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-
-Definition join_countType := @Countable.Pack idomainType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack idomainType xclass xT.
-Definition join_countRingType := @Ring.Pack idomainType xclass xT.
-Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass xT.
-Definition join_countComRingType := @ComRing.Pack idomainType xclass xT.
-Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition countComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition countUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition countComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+
+Definition join_countType := @Countable.Pack idomainType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack idomainType xclass.
+Definition join_countRingType := @Ring.Pack idomainType xclass.
+Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass.
+Definition join_countComRingType := @ComRing.Pack idomainType xclass.
+Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass.
 
 End ClassDef.
 
@@ -482,38 +482,38 @@ Definition base2 R (c : class_of R) := IntegralDomain.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.Field.class_of.
 Local Coercion base2 : class_of >-> IntegralDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Field.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition countComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-
-Definition join_countType := @Countable.Pack fieldType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack fieldType xclass xT.
-Definition join_countRingType := @Ring.Pack fieldType xclass xT.
-Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass xT.
-Definition join_countComRingType := @ComRing.Pack fieldType xclass xT.
-Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass xT.
-Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition countComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition countUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition countComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition countIdomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+
+Definition join_countType := @Countable.Pack fieldType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack fieldType xclass.
+Definition join_countRingType := @Ring.Pack fieldType xclass.
+Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass.
+Definition join_countComRingType := @ComRing.Pack fieldType xclass.
+Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass.
+Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass.
 
 End ClassDef.
 
@@ -579,42 +579,42 @@ Definition base2 R (c : class_of R) := Field.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.DecidableField.class_of.
 Local Coercion base2 : class_of >-> Field.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.DecidableField.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition countComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition countFieldType := @Field.Pack cT xclass xT.
-Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
-
-Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack decFieldType xclass xT.
-Definition join_countRingType := @Ring.Pack decFieldType xclass xT.
-Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass xT.
-Definition join_countComRingType := @ComRing.Pack decFieldType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition countComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition countUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition countComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition countIdomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition countFieldType := @Field.Pack cT xclass.
+Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
+
+Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack decFieldType xclass.
+Definition join_countRingType := @Ring.Pack decFieldType xclass.
+Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass.
+Definition join_countComRingType := @ComRing.Pack decFieldType xclass.
 Definition join_countComUnitRingType :=
-  @ComUnitRing.Pack decFieldType xclass xT.
-Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass xT.
-Definition join_countFieldType := @Field.Pack decFieldType xclass xT.
+  @ComUnitRing.Pack decFieldType xclass.
+Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass.
+Definition join_countFieldType := @Field.Pack decFieldType xclass.
 
 End ClassDef.
 
@@ -685,47 +685,47 @@ Definition base2 R (c : class_of R) := DecidableField.Class (base c) (mixin c).
 Local Coercion base : class_of >-> GRing.ClosedField.class_of.
 Local Coercion base2 : class_of >-> DecidableField.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.ClosedField.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition countZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition countRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition countComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition countFieldType := @Field.Pack cT xclass xT.
-Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
-Definition countDecFieldType := @DecidableField.Pack cT xclass xT.
-Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.
-
-Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass) xT.
-Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass xT.
-Definition join_countRingType := @Ring.Pack closedFieldType xclass xT.
-Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass xT.
-Definition join_countComRingType := @ComRing.Pack closedFieldType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (cnt_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition countZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition countRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition countComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition countUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition countComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition countIdomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition countFieldType := @Field.Pack cT xclass.
+Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
+Definition countDecFieldType := @DecidableField.Pack cT xclass.
+Definition closedFieldType := @GRing.ClosedField.Pack cT xclass.
+
+Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass).
+Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass.
+Definition join_countRingType := @Ring.Pack closedFieldType xclass.
+Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass.
+Definition join_countComRingType := @ComRing.Pack closedFieldType xclass.
 Definition join_countComUnitRingType :=
-  @ComUnitRing.Pack closedFieldType xclass xT.
+  @ComUnitRing.Pack closedFieldType xclass.
 Definition join_countIdomainType :=
-  @IntegralDomain.Pack closedFieldType xclass xT.
-Definition join_countFieldType := @Field.Pack closedFieldType xclass xT.
+  @IntegralDomain.Pack closedFieldType xclass.
+Definition join_countFieldType := @Field.Pack closedFieldType xclass.
 Definition join_countDecFieldType :=
-  @DecidableField.Pack closedFieldType xclass xT.
+  @DecidableField.Pack closedFieldType xclass.
 
 End ClassDef.
 
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 939cd38..3e28760 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -51,14 +51,14 @@ Variable to_choice : forall T, base_of T -> Choice.class_of T.
 Variable base_sort : base_type -> Type.
 
 (* Explicits *)
-Variable Pack : forall T, class_of T -> Type -> type.
+Variable Pack : forall T, class_of T -> type.
 Variable Class : forall T b, mixin_of T (to_choice b) -> class_of T.
 Variable base_class : forall bT, base_of (base_sort bT).
 
 Definition gen_pack T :=
   fun bT b & phant_id (base_class bT) b =>
   fun fT m & phant_id (Finite.class fT) (Finite.Class m) =>
-  Pack (@Class T b m) T.
+  Pack (@Class T b m).
 
 End Generic.
 
@@ -81,21 +81,21 @@ Record class_of M :=
 Local Coercion base : class_of >-> GRing.Zmodule.class_of.
 Local Coercion mixin : class_of >-> mixin_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Zmodule.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
 
-Definition join_finType := @Finite.Pack zmodType (fin_ xclass) xT.
+Definition join_finType := @Finite.Pack zmodType (fin_ xclass).
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -167,23 +167,23 @@ Definition base2 R (c : class_of R) := Zmodule.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Ring.class_of.
 Local Coercion base2 : class_of >-> Zmodule.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Ring.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) cT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass cT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition join_finType := @Finite.Pack ringType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack ringType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition join_finType := @Finite.Pack ringType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack ringType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -272,26 +272,26 @@ Definition base2 R (c : class_of R) := Ring.Class (mixin c).
 Local Coercion base : class_of >-> GRing.ComRing.class_of.
 Local Coercion base2 : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.ComRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition join_finType := @Finite.Pack comRingType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack comRingType xclass xT.
-Definition join_finRingType := @Ring.Pack comRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition join_finType := @Finite.Pack comRingType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack comRingType xclass.
+Definition join_finRingType := @Ring.Pack comRingType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -351,27 +351,27 @@ Definition base2 R (c : class_of R) := Ring.Class (mixin c).
 Local Coercion base : class_of >-> GRing.UnitRing.class_of.
 Local Coercion base2 : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.UnitRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
 
-Definition join_finType := @Finite.Pack unitRingType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack unitRingType xclass xT.
-Definition join_finRingType := @Ring.Pack unitRingType xclass xT.
+Definition join_finType := @Finite.Pack unitRingType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack unitRingType xclass.
+Definition join_finRingType := @Ring.Pack unitRingType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -514,36 +514,36 @@ Local Coercion base : class_of >-> GRing.ComUnitRing.class_of.
 Local Coercion base2 : class_of >-> ComRing.class_of.
 Local Coercion base3 : class_of >-> UnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.ComUnitRing.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition finComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-
-Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass xT.
-Definition join_finRingType := @Ring.Pack comUnitRingType xclass xT.
-Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass xT.
-Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass xT.
-Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass xT.
-Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass xT.
-Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition finComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition finUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+
+Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass.
+Definition join_finRingType := @Ring.Pack comUnitRingType xclass.
+Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass.
+Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass.
+Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass.
+Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass.
+Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -619,36 +619,36 @@ Definition base2 R (c : class_of R) := ComUnitRing.Class (mixin c).
 Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
 Local Coercion base2 : class_of >-> ComUnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition finComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-
-Definition join_finType := @Finite.Pack idomainType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack idomainType xclass xT.
-Definition join_finRingType := @Ring.Pack idomainType xclass xT.
-Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass xT.
-Definition join_finComRingType := @ComRing.Pack idomainType xclass xT.
-Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition finComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition finUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition finComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+
+Definition join_finType := @Finite.Pack idomainType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack idomainType xclass.
+Definition join_finRingType := @Ring.Pack idomainType xclass.
+Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass.
+Definition join_finComRingType := @ComRing.Pack idomainType xclass.
+Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -726,39 +726,39 @@ Definition base2 R (c : class_of R) := IntegralDomain.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Field.class_of.
 Local Coercion base2 : class_of >-> IntegralDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Definition pack := gen_pack Pack Class GRing.Field.class.
 Variable cT : type.
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition finComRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition finIdomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-
-Definition join_finType := @Finite.Pack fieldType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack fieldType xclass xT.
-Definition join_finRingType := @Ring.Pack fieldType xclass xT.
-Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass xT.
-Definition join_finComRingType := @ComRing.Pack fieldType xclass xT.
-Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass xT.
-Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition finComRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition finUnitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition finComUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition finIdomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+
+Definition join_finType := @Finite.Pack fieldType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack fieldType xclass.
+Definition join_finRingType := @Ring.Pack fieldType xclass.
+Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass.
+Definition join_finComRingType := @ComRing.Pack fieldType xclass.
+Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass.
+Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -870,17 +870,17 @@ Module DecField.
 Section Joins.
 
 Variable cT : Field.type.
-Let xT := let: Field.Pack T _ _ := cT in T.
+Let xT := let: Field.Pack T _ := cT in T. 
 Let xclass : Field.class_of xT := Field.class cT.
 
 Definition type := Eval hnf in DecFieldType cT (DecidableFieldMixin cT).
-Definition finType := @Finite.Pack type (fin_ xclass) xT.
-Definition finZmodType := @Zmodule.Pack type xclass xT.
-Definition finRingType := @Ring.Pack type xclass xT.
-Definition finUnitRingType := @UnitRing.Pack type xclass xT.
-Definition finComRingType := @ComRing.Pack type xclass xT.
-Definition finComUnitRingType := @ComUnitRing.Pack type xclass xT.
-Definition finIdomainType := @IntegralDomain.Pack type xclass xT.
+Definition finType := @Finite.Pack type (fin_ xclass).
+Definition finZmodType := @Zmodule.Pack type xclass.
+Definition finRingType := @Ring.Pack type xclass.
+Definition finUnitRingType := @UnitRing.Pack type xclass.
+Definition finComRingType := @ComRing.Pack type xclass.
+Definition finComUnitRingType := @ComUnitRing.Pack type xclass.
+Definition finIdomainType := @IntegralDomain.Pack type xclass.
 Definition baseFinGroupType := base_group type finZmodType finZmodType.
 Definition finGroupType := fin_group baseFinGroupType cT.
 
@@ -915,23 +915,23 @@ Definition base2 R (c : class_of R) := Zmodule.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Lmodule.class_of.
 Local Coercion base2 : class_of >-> Zmodule.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) (cT : type phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition pack := gen_pack (Pack phR) Class (@GRing.Lmodule.class R phR).
-Let xT := let: Pack T _ _ := cT in T.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
-Definition join_finType := @Finite.Pack lmodType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack lmodType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
+Definition join_finType := @Finite.Pack lmodType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack lmodType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -991,33 +991,33 @@ Local Coercion base : class_of >-> GRing.Lalgebra.class_of.
 Local Coercion base2 : class_of >-> Ring.class_of.
 Local Coercion base3 : class_of >-> 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) (cT : type phR).
 Definition pack := gen_pack (Pack phR) Class (@GRing.Lalgebra.class R phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
-Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
-
-Definition join_finType := @Finite.Pack lalgType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack lalgType xclass xT.
-Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass xT.
-Definition join_finRingType := @Ring.Pack lalgType xclass xT.
-Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass xT.
-Definition ljoin_finRingType := @Ring.Pack lmodType xclass xT.
-Definition fljoin_finRingType := @Ring.Pack finLmodType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass.
+
+Definition join_finType := @Finite.Pack lalgType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack lalgType xclass.
+Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass.
+Definition join_finRingType := @Ring.Pack lalgType xclass.
+Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass.
+Definition ljoin_finRingType := @Ring.Pack lmodType xclass.
+Definition fljoin_finRingType := @Ring.Pack finLmodType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -1090,33 +1090,33 @@ Definition base2 M (c : class_of M) := Lalgebra.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Algebra.class_of.
 Local Coercion base2 : class_of >->Lalgebra.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) (cT : type phR).
 Definition pack := gen_pack (Pack phR) Class (@GRing.Algebra.class R phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
-Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
-Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
-Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
-
-Definition join_finType := @Finite.Pack algType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack algType xclass xT.
-Definition join_finRingType := @Ring.Pack algType xclass xT.
-Definition join_finLmodType := @Lmodule.Pack R phR algType xclass xT.
-Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass.
+Definition finLalgType := @Lalgebra.Pack R phR cT xclass.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass.
+
+Definition join_finType := @Finite.Pack algType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack algType xclass.
+Definition join_finRingType := @Ring.Pack algType xclass.
+Definition join_finLmodType := @Lmodule.Pack R phR algType xclass.
+Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -1193,48 +1193,48 @@ Local Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
 Local Coercion base2 : class_of >-> Algebra.class_of.
 Local Coercion base3 : class_of >-> UnitRing.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) (cT : type phR).
 Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition countType := @Countable.Pack cT (fin_ xclass) xT.
-Definition finType := @Finite.Pack cT (fin_ xclass) xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition finZmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition finRingType := @Ring.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
-Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
-Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
-Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
-Definition finAlgType := @Algebra.Pack R phR cT xclass xT.
-Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
-
-Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass) xT.
-Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass xT.
-Definition join_finRingType := @Ring.Pack unitAlgType xclass xT.
-Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass xT.
-Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass xT.
-Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass xT.
-Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass xT.
-Definition  ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass xT.
-Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass xT.
-Definition  njoin_finUnitRingType := @UnitRing.Pack lalgType xclass xT.
-Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass xT.
-Definition  ajoin_finUnitRingType := @UnitRing.Pack algType xclass xT.
-Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass xT.
-Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass xT.
-Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass xT.
-Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (fin_ xclass).
+Definition finType := @Finite.Pack cT (fin_ xclass).
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition finZmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition finRingType := @Ring.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition finUnitRingType := @UnitRing.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass.
+Definition finLalgType := @Lalgebra.Pack R phR cT xclass.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass.
+Definition finAlgType := @Algebra.Pack R phR cT xclass.
+Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass.
+
+Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass).
+Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass.
+Definition join_finRingType := @Ring.Pack unitAlgType xclass.
+Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass.
+Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass.
+Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass.
+Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass.
+Definition  ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass.
+Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass.
+Definition  njoin_finUnitRingType := @UnitRing.Pack lalgType xclass.
+Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass.
+Definition  ajoin_finUnitRingType := @UnitRing.Pack algType xclass.
+Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass.
+Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass.
+Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass.
+Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass.
 
 Definition baseFinGroupType := base_group cT zmodType finType.
 Definition finGroupType := fin_group baseFinGroupType zmodType.
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 8745049..7e708ca 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -110,11 +110,11 @@ Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T).
 Record zmod_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
   (zc : GRing.Zmodule.class_of Q) := ZmodQuotMixinPack {
     zmod_eq_quot_mixin :> eq_quot_mixin_of eqT qc zc;
-    _ : \pi_(QuotTypePack qc Q) zeroT = 0 :> GRing.Zmodule.Pack zc Q;
-    _ : {morph \pi_(QuotTypePack qc Q) : x /
-         oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc Q) x};
-    _ : {morph \pi_(QuotTypePack qc Q) : x y /
-         addT x y >-> @GRing.add (GRing.Zmodule.Pack zc Q) x y}
+    _ : \pi_(QuotTypePack qc) zeroT = 0 :> GRing.Zmodule.Pack zc;
+    _ : {morph \pi_(QuotTypePack qc) : x /
+         oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc) x};
+    _ : {morph \pi_(QuotTypePack qc) : x y /
+         addT x y >-> @GRing.add (GRing.Zmodule.Pack zc) x y}
 }.
 
 Record zmod_quot_class_of (Q : Type) : Type := ZmodQuotClass {
@@ -127,25 +127,25 @@ Record zmod_quot_class_of (Q : Type) : Type := ZmodQuotClass {
 Structure zmodQuotType : Type := ZmodQuotTypePack {
   zmod_quot_sort :> Type;
   _ : zmod_quot_class_of zmod_quot_sort;
-  _ : Type
+ 
 }.
 
 Implicit Type zqT : zmodQuotType.
 
 Definition zmod_quot_class zqT : zmod_quot_class_of zqT :=
-  let: ZmodQuotTypePack _ cT _ as qT' := zqT return zmod_quot_class_of qT' in cT.
+  let: ZmodQuotTypePack _ cT as qT' := zqT return zmod_quot_class_of qT' in cT.
 
 Definition zmod_eq_quot_class zqT (zqc : zmod_quot_class_of zqT) :
   eq_quot_class_of eqT zqT := EqQuotClass zqc.
 
-Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT) zqT.
+Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT).
 Canonical zmodQuotType_choiceType zqT :=
-  Choice.Pack (zmod_quot_class zqT) zqT.
+  Choice.Pack (zmod_quot_class zqT).
 Canonical zmodQuotType_zmodType zqT :=
-  GRing.Zmodule.Pack (zmod_quot_class zqT) zqT.
-Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT) zqT.
+  GRing.Zmodule.Pack (zmod_quot_class zqT).
+Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT).
 Canonical zmodQuotType_eqQuotType zqT := EqQuotTypePack
-  (zmod_eq_quot_class (zmod_quot_class zqT)) zqT.
+  (zmod_eq_quot_class (zmod_quot_class zqT)).
 
 Coercion zmodQuotType_eqType : zmodQuotType >-> eqType.
 Coercion zmodQuotType_choiceType : zmodQuotType >-> choiceType.
@@ -156,7 +156,7 @@ Coercion zmodQuotType_eqQuotType : zmodQuotType >-> eqQuotType.
 Definition ZmodQuotType_pack Q :=
   fun (qT : quotType T) (zT : zmodType) qc zc
   of phant_id (quot_class qT) qc & phant_id (GRing.Zmodule.class zT) zc =>
-    fun m => ZmodQuotTypePack (@ZmodQuotClass Q qc zc m) Q.
+    fun m => ZmodQuotTypePack (@ZmodQuotClass Q qc zc m).
 
 Definition ZmodQuotMixin_pack Q :=
   fun (qT : eqQuotType eqT) (qc : eq_quot_class_of eqT Q)
@@ -165,7 +165,7 @@ Definition ZmodQuotMixin_pack Q :=
     fun e m0 mN mD => @ZmodQuotMixinPack Q qc zc e m0 mN mD.
 
 Definition ZmodQuotType_clone (Q : Type) qT cT
-  of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT Q.
+  of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT.
 
 Lemma zmod_quot_mixinP zqT :
   zmod_quot_mixin_of (zmod_quot_class zqT) (zmod_quot_class zqT).
@@ -216,9 +216,9 @@ Variables (oneT : T) (mulT : T -> T -> T).
 Record ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
   (rc : GRing.Ring.class_of Q) := RingQuotMixinPack {
     ring_zmod_quot_mixin :> zmod_quot_mixin_of eqT zeroT oppT addT qc rc;
-    _ : \pi_(QuotTypePack qc Q) oneT = 1 :> GRing.Ring.Pack rc Q;
-    _ : {morph \pi_(QuotTypePack qc Q) : x y /
-         mulT x y >-> @GRing.mul (GRing.Ring.Pack rc Q) x y}
+    _ : \pi_(QuotTypePack qc) oneT = 1 :> GRing.Ring.Pack rc;
+    _ : {morph \pi_(QuotTypePack qc) : x y /
+         mulT x y >-> @GRing.mul (GRing.Ring.Pack rc) x y}
 }.
 
 Record ring_quot_class_of (Q : Type) : Type := RingQuotClass {
@@ -231,30 +231,30 @@ Record ring_quot_class_of (Q : Type) : Type := RingQuotClass {
 Structure ringQuotType : Type := RingQuotTypePack {
   ring_quot_sort :> Type;
   _ : ring_quot_class_of ring_quot_sort;
-  _ : Type
+ 
 }.
 
 Implicit Type rqT : ringQuotType.
 
 Definition ring_quot_class rqT : ring_quot_class_of rqT :=
-  let: RingQuotTypePack _ cT _ as qT' := rqT return ring_quot_class_of qT' in cT.
+  let: RingQuotTypePack _ cT as qT' := rqT return ring_quot_class_of qT' in cT.
 
 Definition ring_zmod_quot_class rqT (rqc : ring_quot_class_of rqT) :
   zmod_quot_class_of eqT zeroT oppT addT rqT := ZmodQuotClass rqc.
 Definition ring_eq_quot_class rqT (rqc : ring_quot_class_of rqT) :
   eq_quot_class_of eqT rqT := EqQuotClass rqc.
 
-Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT) rqT.
-Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT) rqT.
+Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT).
+Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT).
 Canonical ringQuotType_zmodType rqT :=
-  GRing.Zmodule.Pack (ring_quot_class rqT) rqT.
+  GRing.Zmodule.Pack (ring_quot_class rqT).
 Canonical ringQuotType_ringType rqT :=
-  GRing.Ring.Pack (ring_quot_class rqT) rqT.
-Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT) rqT.
+  GRing.Ring.Pack (ring_quot_class rqT).
+Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT).
 Canonical ringQuotType_eqQuotType rqT :=
-  EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)) rqT.
+  EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)).
 Canonical ringQuotType_zmodQuotType rqT :=
-  ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)) rqT.
+  ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)).
 
 Coercion ringQuotType_eqType : ringQuotType >-> eqType.
 Coercion ringQuotType_choiceType : ringQuotType >-> choiceType.
@@ -267,7 +267,7 @@ Coercion ringQuotType_zmodQuotType : ringQuotType >-> zmodQuotType.
 Definition RingQuotType_pack Q :=
   fun (qT : quotType T) (zT : ringType) qc rc
   of phant_id (quot_class qT) qc & phant_id (GRing.Ring.class zT) rc =>
-    fun m => RingQuotTypePack (@RingQuotClass Q qc rc m) Q.
+    fun m => RingQuotTypePack (@RingQuotClass Q qc rc m).
 
 Definition RingQuotMixin_pack Q :=
   fun (qT : zmodQuotType eqT zeroT oppT addT) =>
@@ -277,7 +277,7 @@ Definition RingQuotMixin_pack Q :=
     fun mZ m1 mM => @RingQuotMixinPack Q qc rc mZ m1 mM.
 
 Definition RingQuotType_clone (Q : Type) qT cT
-  of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT Q.
+  of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT.
 
 Lemma ring_quot_mixinP rqT :
   ring_quot_mixin_of (ring_quot_class rqT) (ring_quot_class rqT).
@@ -327,10 +327,10 @@ Record unit_ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
   (rc : GRing.UnitRing.class_of Q) := UnitRingQuotMixinPack {
     unit_ring_zmod_quot_mixin :>
         ring_quot_mixin_of eqT zeroT oppT addT oneT mulT qc rc;
-    _ : {mono \pi_(QuotTypePack qc Q) : x /
-         unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc Q)};
-    _ : {morph \pi_(QuotTypePack qc Q) : x /
-         invT x >-> @GRing.inv (GRing.UnitRing.Pack rc Q) x}
+    _ : {mono \pi_(QuotTypePack qc) : x /
+         unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc)};
+    _ : {morph \pi_(QuotTypePack qc) : x /
+         invT x >-> @GRing.inv (GRing.UnitRing.Pack rc) x}
 }.
 
 Record unit_ring_quot_class_of (Q : Type) : Type := UnitRingQuotClass {
@@ -343,13 +343,13 @@ Record unit_ring_quot_class_of (Q : Type) : Type := UnitRingQuotClass {
 Structure unitRingQuotType : Type := UnitRingQuotTypePack {
   unit_ring_quot_sort :> Type;
   _ : unit_ring_quot_class_of unit_ring_quot_sort;
-  _ : Type
+ 
 }.
 
 Implicit Type rqT : unitRingQuotType.
 
 Definition unit_ring_quot_class rqT : unit_ring_quot_class_of rqT :=
-  let: UnitRingQuotTypePack _ cT _ as qT' := rqT
+  let: UnitRingQuotTypePack _ cT as qT' := rqT
     return unit_ring_quot_class_of qT' in cT.
 
 Definition unit_ring_ring_quot_class rqT (rqc : unit_ring_quot_class_of rqT) :
@@ -360,23 +360,23 @@ Definition unit_ring_eq_quot_class rqT (rqc : unit_ring_quot_class_of rqT) :
   eq_quot_class_of eqT rqT := EqQuotClass rqc.
 
 Canonical unitRingQuotType_eqType rqT :=
-  Equality.Pack (unit_ring_quot_class rqT) rqT.
+  Equality.Pack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_choiceType rqT :=
-  Choice.Pack (unit_ring_quot_class rqT) rqT.
+  Choice.Pack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_zmodType rqT :=
-  GRing.Zmodule.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.Zmodule.Pack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_ringType rqT :=
-  GRing.Ring.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.Ring.Pack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_unitRingType rqT :=
-  GRing.UnitRing.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.UnitRing.Pack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_quotType rqT :=
-  QuotTypePack (unit_ring_quot_class rqT) rqT.
+  QuotTypePack (unit_ring_quot_class rqT).
 Canonical unitRingQuotType_eqQuotType rqT :=
-  EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)) rqT.
+  EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)).
 Canonical unitRingQuotType_zmodQuotType rqT :=
-  ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)) rqT.
+  ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)).
 Canonical unitRingQuotType_ringQuotType rqT :=
-  RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)) rqT.
+  RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)).
 
 Coercion unitRingQuotType_eqType : unitRingQuotType >-> eqType.
 Coercion unitRingQuotType_choiceType : unitRingQuotType >-> choiceType.
@@ -391,7 +391,7 @@ Coercion unitRingQuotType_ringQuotType : unitRingQuotType >-> ringQuotType.
 Definition UnitRingQuotType_pack Q :=
   fun (qT : quotType T) (rT : unitRingType) qc rc
   of phant_id (quot_class qT) qc & phant_id (GRing.UnitRing.class rT) rc =>
-    fun m => UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m) Q.
+    fun m => UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m).
 
 Definition UnitRingQuotMixin_pack Q :=
   fun (qT : ringQuotType eqT zeroT oppT addT oneT mulT) =>
@@ -401,7 +401,7 @@ Definition UnitRingQuotMixin_pack Q :=
     fun mR mU mV => @UnitRingQuotMixinPack Q qc rc mR mU mV.
 
 Definition UnitRingQuotType_clone (Q : Type) qT cT
-  of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT Q.
+  of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT.
 
 Lemma unit_ring_quot_mixinP rqT :
   unit_ring_quot_mixin_of (unit_ring_quot_class rqT) (unit_ring_quot_class rqT).
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 6df490d..5542959 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -626,19 +626,19 @@ Section ClassDef.
 Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
 Local Coercion base : class_of >-> Choice.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack m :=
-  fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.
+  fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
 
 End ClassDef.
 
@@ -892,33 +892,32 @@ Record mixin_of (R : zmodType) : Type := Mixin {
 
 Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 :=
   let _ := @Mixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 in
-  @Mixin (Zmodule.Pack (Zmodule.class R) R) _ _
+  @Mixin (Zmodule.Pack (Zmodule.class R)) _ _
      mulA mul1x mulx1 mul_addl mul_addr nz1.
 
 Section ClassDef.
 
 Record class_of (R : Type) : Type := Class {
   base : Zmodule.class_of R;
-  mixin : mixin_of (Zmodule.Pack base R)
+  mixin : mixin_of (Zmodule.Pack base)
 }.
 Local Coercion base : class_of >-> Zmodule.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-
-Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0)) :=
   fun bT b & phant_id (Zmodule.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
 
 End ClassDef.
 
@@ -1504,26 +1503,25 @@ Variable R : ringType.
 
 Structure class_of V := Class {
   base : Zmodule.class_of V;
-  mixin : mixin_of R (Zmodule.Pack base V)
+  mixin : mixin_of R (Zmodule.Pack base)
 }.
 Local Coercion base : class_of >-> Zmodule.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.
 Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ as cT' := 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 as cT' := 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 pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0)) :=
   fun bT b & phant_id (Zmodule.class 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 := @Zmodule.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
 
 End ClassDef.
 
@@ -1660,33 +1658,33 @@ Variable R : ringType.
 
 Record class_of (T : Type) : Type := Class {
   base : Ring.class_of T;
-  mixin : Lmodule.mixin_of R (Zmodule.Pack base T);
-  ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin) T) (Ring.mul base)
+  mixin : Lmodule.mixin_of R (Zmodule.Pack base);
+  ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin)) (Ring.mul base)
 }.
 Definition base2 R m := Lmodule.Class (@mixin R m).
 Local Coercion base : class_of >-> Ring.class_of.
 Local Coercion base2 : class_of >-> 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.
 Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ as cT' := 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 as cT' := 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 pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0 T) mul0) :=
+Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) :=
   fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) =>
   fun mT m & phant_id (@Lmodule.class R phR mT) (@Lmodule.Class R T b m) =>
   fun ax & phant_id axT ax =>
-  Pack (Phant R) (@Class T b m ax) T.
+  Pack (Phant R) (@Class T b m ax).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition lmodType := @Lmodule.Pack R phR cT xclass.
+Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass.
 
 End ClassDef.
 
@@ -2472,22 +2470,22 @@ Record class_of R :=
   Class {base : Ring.class_of R; mixin : commutative (Ring.mul base)}.
 Local Coercion base : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack mul0 (m0 : @commutative T T mul0) :=
   fun bT b & phant_id (Ring.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
 
 End ClassDef.
 
@@ -2630,28 +2628,28 @@ Variable R : ringType.
 
 Record class_of (T : Type) : Type := Class {
   base : Lalgebra.class_of R T;
-  mixin : axiom (Lalgebra.Pack _ base T)
+  mixin : axiom (Lalgebra.Pack _ base)
 }.
 Local Coercion base : class_of >-> Lalgebra.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.
 Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ as cT' := 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 as cT' := 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 pack b0 (ax0 : @axiom R b0) :=
   fun bT b & phant_id (@Lalgebra.class R phR bT) b =>
-  fun   ax & phant_id ax0 ax => Pack phR (@Class T b ax) T.
+  fun   ax & phant_id ax0 ax => Pack phR (@Class T b ax).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition lmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass.
 
 End ClassDef.
 
@@ -2744,32 +2742,32 @@ Record mixin_of (R : ringType) : Type := Mixin {
 
 Definition EtaMixin R unit inv mulVr mulrV unitP inv_out :=
   let _ := @Mixin R unit inv mulVr mulrV unitP inv_out in
-  @Mixin (Ring.Pack (Ring.class R) R) unit inv mulVr mulrV unitP inv_out.
+  @Mixin (Ring.Pack (Ring.class R)) unit inv mulVr mulrV unitP inv_out.
 
 Section ClassDef.
 
 Record class_of (R : Type) : Type := Class {
   base : Ring.class_of R;
-  mixin : mixin_of (Ring.Pack base R)
+  mixin : mixin_of (Ring.Pack base)
 }.
 Local Coercion base : class_of >-> Ring.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0)) :=
   fun bT b & phant_id (Ring.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
 
 End ClassDef.
 
@@ -3078,31 +3076,31 @@ Section ClassDef.
 
 Record class_of (R : Type) : Type := Class {
   base : ComRing.class_of R;
-  mixin : UnitRing.mixin_of (Ring.Pack base R)
+  mixin : UnitRing.mixin_of (Ring.Pack base)
 }.
 Local Coercion base : class_of >-> ComRing.class_of.
 Definition base2 R m := UnitRing.Class (@mixin R m).
 Local Coercion base2 : class_of >-> UnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) =>
   fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
-  Pack (@Class T b m) T.
+  Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition com_unitRingType := @UnitRing.Pack comRingType xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition com_unitRingType := @UnitRing.Pack comRingType xclass.
 
 End ClassDef.
 
@@ -3142,35 +3140,35 @@ Variable R : ringType.
 
 Record class_of (T : Type) : Type := Class {
   base : Algebra.class_of R T;
-  mixin : GRing.UnitRing.mixin_of (Ring.Pack base T)
+  mixin : GRing.UnitRing.mixin_of (Ring.Pack base)
 }.
 Definition base2 R m := UnitRing.Class (@mixin R m).
 Local Coercion base : class_of >-> Algebra.class_of.
 Local Coercion base2 : class_of >-> UnitRing.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.
 Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+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 : Algebra.class_of R T) =>
   fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m =>
-  Pack (Phant R) (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
-Definition algType := @Algebra.Pack R phR cT xclass xT.
-Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass xT.
-Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass xT.
-Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass xT.
+  Pack (Phant R) (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition unitRingType := @UnitRing.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.
+Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass.
+Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass.
+Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass.
 
 End ClassDef.
 
@@ -4351,28 +4349,28 @@ Definition axiom (R : ringType) :=
 Section ClassDef.
 
 Record class_of (R : Type) : Type :=
-  Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base R)}.
+  Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base)}.
 Local Coercion base : class_of >-> ComUnitRing.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
+Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
   fun bT b & phant_id (ComUnitRing.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
 
 End ClassDef.
 
@@ -4569,30 +4567,30 @@ Section ClassDef.
 
 Record class_of (F : Type) : Type := Class {
   base : IntegralDomain.class_of F;
-  mixin : mixin_of (UnitRing.Pack base F)
+  mixin : mixin_of (UnitRing.Pack base)
 }.
 Local Coercion base : class_of >-> IntegralDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
   fun bT b & phant_id (IntegralDomain.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
 
 End ClassDef.
 
@@ -4826,30 +4824,30 @@ Record mixin_of (R : unitRingType) : Type :=
 Section ClassDef.
 
 Record class_of (F : Type) : Type :=
-  Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base F)}.
+  Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base)}.
 Local Coercion base : class_of >-> Field.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
   fun bT b & phant_id (Field.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @Field.Pack cT xclass xT.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @Field.Pack cT xclass.
 
 End ClassDef.
 
@@ -5068,34 +5066,34 @@ Definition axiom (R : ringType) :=
 Section ClassDef.
 
 Record class_of (F : Type) : Type :=
-  Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base F)}.
+  Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base)}.
 Local Coercion base : class_of >-> DecidableField.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
+Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
   fun bT b & phant_id (DecidableField.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
 
 (* There should eventually be a constructor from polynomial resolution *)
 (* that builds the DecidableField mixin using QE.                      *)
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @Field.Pack cT xclass xT.
-Definition decFieldType := @DecidableField.Pack cT class xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @Field.Pack cT xclass.
+Definition decFieldType := @DecidableField.Pack cT class.
 
 End ClassDef.
 
@@ -5183,7 +5181,7 @@ Variables (ringS : subringPred S) (kS : keyed_pred ringS).
 
 Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) :=
   let cast mV := let: erefl in _ = T := VeqT return Zmodule.class_of T in mV in
-  Zmodule.Pack (cast (Zmodule.class V)) T.
+  Zmodule.Pack (cast (Zmodule.class V)).
 
 Variable (T : subType (mem kS)) (V : zmodType) (VeqT: V = T :> Type).
 
@@ -5266,7 +5264,7 @@ Section UnitRing.
 
 Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) :=
   let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in
-  Ring.Pack (cast (Ring.class Q)) T.
+  Ring.Pack (cast (Ring.class Q)).
 
 Variables (R : unitRingType) (S : predPredType R).
 Variables (ringS : divringPred S) (kS : keyed_pred ringS).
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 5c6f098..ae0c00b 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -163,7 +163,7 @@ Record mixin_of (R : ringType) := Mixin {
   _ : forall x y, (lt_op x y) = (y != x) && (le_op x y)
 }.
 
-Local Notation ring_for T b := (@GRing.Ring.Pack T b T).
+Local Notation ring_for T b := (@GRing.Ring.Pack T b).
 
 (* Base interface. *)
 Module NumDomain.
@@ -175,25 +175,26 @@ Record class_of T := Class {
   mixin : mixin_of (ring_for T base)
 }.
 Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _  as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c  as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
-Definition clone c of phant_id class c := @Pack T c T.
+
+Definition clone c of phant_id class c := @Pack T c.
 Definition pack b0 (m0 : mixin_of (ring_for T b0)) :=
   fun bT b & phant_id (GRing.IntegralDomain.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
+  fun    m & phant_id m0 m => Pack (@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 ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
 
 End ClassDef.
 
@@ -345,7 +346,7 @@ Definition real_closed_axiom : Prop :=
 
 End ExtensionAxioms.
 
-Local Notation num_for T b := (@NumDomain.Pack T b T).
+Local Notation num_for T b := (@NumDomain.Pack T b).
 
 (* The rest of the numbers interface hierarchy. *)
 Module NumField.
@@ -358,28 +359,29 @@ Definition base2 R (c : class_of R) := NumDomain.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Field.class_of.
 Local Coercion base2 : class_of >-> NumDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
+
 Definition pack :=
   fun bT b & phant_id (GRing.Field.class bT) (b : GRing.Field.class_of T) =>
   fun mT m & phant_id (NumDomain.class mT) (@NumDomain.Class T b m) =>
-  Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition join_numDomainType := @NumDomain.Pack fieldType xclass xT.
+  Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition join_numDomainType := @NumDomain.Pack fieldType xclass.
 
 End ClassDef.
 
@@ -436,36 +438,37 @@ Definition base2 R (c : class_of R) := NumField.Class (mixin c).
 Local Coercion base : class_of >-> GRing.ClosedField.class_of.
 Local Coercion base2 : class_of >-> NumField.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
+
 Definition pack :=
   fun bT b & phant_id (GRing.ClosedField.class bT)
                       (b : GRing.ClosedField.class_of T) =>
   fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) =>
-  fun mc => Pack (@Class T b m mc) T.
-Definition clone := fun b & phant_id class (b : class_of T) => Pack b T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition numFieldType := @NumField.Pack cT xclass xT.
-Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
-Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.
-Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass xT.
-Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass xT.
-Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass xT.
-Definition join_numFieldType := @NumField.Pack closedFieldType xclass xT.
+  fun mc => Pack (@Class T b m mc).
+Definition clone := fun b & phant_id class (b : class_of T) => Pack b.
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition numFieldType := @NumField.Pack cT xclass.
+Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
+Definition closedFieldType := @GRing.ClosedField.Pack cT xclass.
+Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass.
+Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass.
+Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass.
+Definition join_numFieldType := @NumField.Pack closedFieldType xclass.
 
 End ClassDef.
 
@@ -524,26 +527,27 @@ Record class_of R :=
   Class {base : NumDomain.class_of R; _ : @real_axiom (num_for R base)}.
 Local Coercion base : class_of >-> NumDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
-Definition clone c of phant_id class c := @Pack T c T.
+
+Definition clone c of phant_id class c := @Pack T c.
 Definition pack b0 (m0 : real_axiom (num_for T b0)) :=
   fun bT b & phant_id (NumDomain.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
 
 End ClassDef.
 
@@ -590,30 +594,31 @@ Definition base2 R (c : class_of R) := RealDomain.Class (@mixin R c).
 Local Coercion base : class_of >-> NumField.class_of.
 Local Coercion base2 : class_of >-> RealDomain.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
+
 Definition pack :=
   fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) =>
   fun mT m & phant_id (RealDomain.class mT) (@RealDomain.Class T b m) =>
-  Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
-Definition realDomainType := @RealDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition numFieldType := @NumField.Pack cT xclass xT.
-Definition join_realDomainType := @RealDomain.Pack numFieldType xclass xT.
+  Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
+Definition realDomainType := @RealDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition numFieldType := @NumField.Pack cT xclass.
+Definition join_realDomainType := @RealDomain.Pack numFieldType xclass.
 
 End ClassDef.
 
@@ -663,30 +668,31 @@ Record class_of R :=
   Class { base : RealField.class_of R; _ : archimedean_axiom (num_for R base) }.
 Local Coercion base : class_of >-> RealField.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
-Definition clone c of phant_id class c := @Pack T c T.
+
+Definition clone c of phant_id class c := @Pack T c.
 Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) :=
   fun bT b & phant_id (RealField.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
-Definition realDomainType := @RealDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition numFieldType := @NumField.Pack cT xclass xT.
-Definition realFieldType := @RealField.Pack cT xclass xT.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
+Definition realDomainType := @RealDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition numFieldType := @NumField.Pack cT xclass.
+Definition realFieldType := @RealField.Pack cT xclass.
 
 End ClassDef.
 
@@ -739,30 +745,31 @@ Record class_of R :=
   Class { base : RealField.class_of R; _ : real_closed_axiom (num_for R base) }.
 Local Coercion base : class_of >-> RealField.class_of.
 
-Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
-Definition clone c of phant_id class c := @Pack T c T.
+
+Definition clone c of phant_id class c := @Pack T c.
 Definition pack b0 (m0 : real_closed_axiom (num_for T b0)) :=
   fun bT b & phant_id (RealField.class bT) b =>
-  fun    m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @NumDomain.Pack cT xclass xT.
-Definition realDomainType := @RealDomain.Pack cT xclass xT.
-Definition fieldType := @GRing.Field.Pack cT xclass xT.
-Definition numFieldType := @NumField.Pack cT xclass xT.
-Definition realFieldType := @RealField.Pack cT xclass xT.
+  fun    m & phant_id m0 m => Pack (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @NumDomain.Pack cT xclass.
+Definition realDomainType := @RealDomain.Pack cT xclass.
+Definition fieldType := @GRing.Field.Pack cT xclass.
+Definition numFieldType := @NumField.Pack cT xclass.
+Definition realFieldType := @RealField.Pack cT xclass.
 
 End ClassDef.
 
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)).