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

Remove `_ : Type` from packed classes

15 files changed, 920 insertions, 919 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)).
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 7e86d3c..53a27f0 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -119,7 +119,7 @@ Definition BaseType T :=
   fun c vAm & phant_id c (GRing.UnitRing.Class (BaseMixin vAm)) =>
   fun (vT : vectType K) & phant vT
      & phant_id (Vector.mixin (Vector.class vT)) vAm =>
-  @GRing.UnitRing.Pack T c T.
+  @GRing.UnitRing.Pack T c.
 
 End DefaultBase.
 
@@ -129,41 +129,41 @@ Implicit Type phR : phant R.
 
 Record class_of A := Class {
   base1 : GRing.UnitAlgebra.class_of R A;
-  mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1 A)
+  mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1)
 }.
 Local Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
 Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
 Local Coercion base2 : class_of >-> Vector.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.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c := 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.UnitAlgebra.class R phR bT)
                       (b : GRing.UnitAlgebra.class_of R T) =>
   fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b 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 := @GRing.Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
-Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
-Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
-Definition vectType := @Vector.Pack R phR cT xclass cT.
-Definition vect_ringType := @GRing.Ring.Pack vectType xclass xT.
-Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass xT.
-Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass xT.
-Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass xT.
-Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass xT.
+  Pack (Phant R) (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass.
+Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass.
+Definition vectType := @Vector.Pack R phR cT xclass.
+Definition vect_ringType := @GRing.Ring.Pack vectType xclass.
+Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass.
+Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass.
+Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass.
+Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass.
 
 End ClassDef.
 
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 881b888..99db561 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -99,8 +99,8 @@ Variable R : ringType.
 Record class_of T := Class {
   base : Falgebra.class_of R T;
   comm_ext : commutative (Ring.mul base);
-  idomain_ext : IntegralDomain.axiom (Ring.Pack base T);
-  field_ext : Field.mixin_of (UnitRing.Pack base T)
+  idomain_ext : IntegralDomain.axiom (Ring.Pack base);
+  field_ext : Field.mixin_of (UnitRing.Pack base)
 }.
 
 Local Coercion base : class_of >-> Falgebra.class_of.
@@ -117,12 +117,12 @@ Local Coercion base2 : class_of >-> ComUnitRing.class_of.
 Local Coercion base3 : class_of >-> IntegralDomain.class_of.
 Local Coercion base4 : class_of >-> Field.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.
-Let xT := let: Pack T _ _ := cT in T.
+Definition class := let: Pack _ c :=  cT return class_of cT in c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack :=
@@ -131,59 +131,59 @@ Definition pack :=
                (b : Falgebra.class_of R T) =>
   fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T
         (@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b
-          Cm) b) IDm) Fm) => Pack phR (@Class T b Cm IDm Fm) T.
+          Cm) b) IDm) Fm) => Pack phR (@Class T b Cm IDm Fm).
 
 Definition pack_eta K :=
   let cK := Field.class K in let Cm := ComRing.mixin cK in
   let IDm := IntegralDomain.mixin cK in let Fm := Field.mixin cK in
   fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT) b =>
-  fun cT_ & phant_id (@Class T b) cT_ => @Pack phR T (cT_ Cm IDm Fm) 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 comRingType := @ComRing.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 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 unitAlgType := @UnitAlgebra.Pack R phR cT xclass xT.
-Definition vectType := @Vector.Pack R phR cT xclass xT.
-Definition FalgType := @Falgebra.Pack R phR cT xclass xT.
-
-Definition Falg_comRingType := @ComRing.Pack FalgType xclass xT.
-Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass xT.
-Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass xT.
-Definition Falg_fieldType := @Field.Pack FalgType xclass xT.
-
-Definition vect_comRingType := @ComRing.Pack vectType xclass xT.
-Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass xT.
-Definition vect_idomainType := @IntegralDomain.Pack vectType xclass xT.
-Definition vect_fieldType := @Field.Pack vectType xclass xT.
-
-Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass xT.
-Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass xT.
-Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass xT.
-Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass xT.
-
-Definition alg_comRingType := @ComRing.Pack algType xclass xT.
-Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass xT.
-Definition alg_idomainType := @IntegralDomain.Pack algType xclass xT.
-Definition alg_fieldType := @Field.Pack algType xclass xT.
-
-Definition lalg_comRingType := @ComRing.Pack lalgType xclass xT.
-Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass xT.
-Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass xT.
-Definition lalg_fieldType := @Field.Pack lalgType xclass xT.
-
-Definition lmod_comRingType := @ComRing.Pack lmodType xclass xT.
-Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass xT.
-Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass xT.
-Definition lmod_fieldType := @Field.Pack lmodType xclass xT.
+  fun cT_ & phant_id (@Class T b) cT_ => @Pack phR T (cT_ Cm IDm Fm).
+
+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 comRingType := @ComRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @Field.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 unitAlgType := @UnitAlgebra.Pack R phR cT xclass.
+Definition vectType := @Vector.Pack R phR cT xclass.
+Definition FalgType := @Falgebra.Pack R phR cT xclass.
+
+Definition Falg_comRingType := @ComRing.Pack FalgType xclass.
+Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass.
+Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass.
+Definition Falg_fieldType := @Field.Pack FalgType xclass.
+
+Definition vect_comRingType := @ComRing.Pack vectType xclass.
+Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass.
+Definition vect_idomainType := @IntegralDomain.Pack vectType xclass.
+Definition vect_fieldType := @Field.Pack vectType xclass.
+
+Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass.
+Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass.
+Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass.
+Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass.
+
+Definition alg_comRingType := @ComRing.Pack algType xclass.
+Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass.
+Definition alg_idomainType := @IntegralDomain.Pack algType xclass.
+Definition alg_fieldType := @Field.Pack algType xclass.
+
+Definition lalg_comRingType := @ComRing.Pack lalgType xclass.
+Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass.
+Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass.
+Definition lalg_fieldType := @Field.Pack lalgType xclass.
+
+Definition lmod_comRingType := @ComRing.Pack lmodType xclass.
+Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass.
+Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass.
+Definition lmod_fieldType := @Field.Pack lmodType xclass.
 
 End FieldExt.
 
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 2421b16..4197a2e 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -138,7 +138,7 @@ Variables (F : finFieldType) (T : finType).
 Section Vector.
 
 Variable cvT : Vector.class_of F T.
-Let vT := Vector.Pack (Phant F) cvT T.
+Let vT := Vector.Pack (Phant F) cvT.
 
 Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
 Proof.
@@ -159,7 +159,7 @@ Proof. by apply: eq_card => v; rewrite (@memvf _ vT). Qed.
 End Vector.
 
 Variable caT : Falgebra.class_of F T.
-Let aT := Falgebra.Pack (Phant F) caT T.
+Let aT := Falgebra.Pack (Phant F) caT.
 
 Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.
 Proof. by rewrite card_vspace (dimv1 aT). Qed.
@@ -691,7 +691,7 @@ Definition FinDomainFieldType : finFieldType :=
   let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in
   let field_class := @GRing.Field.Class R dom_class finDomain_field in
   let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in
-  FinRing.Field.Pack finfield_class R.
+  FinRing.Field.Pack finfield_class.
 
 Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
    let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 2ed40e1..252868d 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -345,38 +345,38 @@ Definition axiom (L : fieldExtType F) :=
   exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
 
 Record class_of (L : Type) : Type :=
-  Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base L)}.
+  Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}.
 Local Coercion base : class_of >-> FieldExt.class_of.
 
-Structure type (phF : phant F) := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type (phF : phant F) := Pack {sort; _ : class_of sort}.
 Local Coercion sort : type >-> Sortclass.
 Variable (phF : phant F) (T : Type) (cT : type phF).
-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 phF T c T.
+Definition clone c of phant_id class c := @Pack phF T c.
 
-Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0 T)) :=
+Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0)) :=
  fun bT b & phant_id (@FieldExt.class F phF bT) b =>
- fun   ax & phant_id ax0 ax => Pack (Phant F) (@Class T b ax) 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 comRingType := @ComRing.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 lmodType := @Lmodule.Pack F phF cT xclass xT.
-Definition lalgType := @Lalgebra.Pack F phF cT xclass xT.
-Definition algType := @Algebra.Pack F phF cT xclass xT.
-Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass xT.
-Definition vectType := @Vector.Pack F phF cT xclass xT.
-Definition FalgType := @Falgebra.Pack F phF cT xclass xT.
-Definition fieldExtType := @FieldExt.Pack F phF cT xclass xT.
+ fun   ax & phant_id ax0 ax => Pack (Phant F) (@Class T b ax).
+
+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 comRingType := @ComRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @Field.Pack cT xclass.
+Definition lmodType := @Lmodule.Pack F phF cT xclass.
+Definition lalgType := @Lalgebra.Pack F phF cT xclass.
+Definition algType := @Algebra.Pack F phF cT xclass.
+Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass.
+Definition vectType := @Vector.Pack F phF cT xclass.
+Definition FalgType := @Falgebra.Pack F phF cT xclass.
+Definition fieldExtType := @FieldExt.Pack F phF cT xclass.
 
 End ClassDef.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index a68bc9f..19cefcd 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -302,10 +302,10 @@ Local Notation T := (arg_sort bT).
 Local Notation rT := (sort bT).
 Local Notation class := (finClass bT).
 
-Canonical eqType := Equality.Pack class rT.
-Canonical choiceType := Choice.Pack class rT.
-Canonical countType := Countable.Pack class rT.
-Canonical finType := Finite.Pack class rT.
+Canonical eqType := Equality.Pack class.
+Canonical choiceType := Choice.Pack class.
+Canonical countType := Countable.Pack class.
+Canonical finType := Finite.Pack class.
 Definition arg_eqType := Eval hnf in [eqType of T].
 Definition arg_choiceType := Eval hnf in [choiceType of T].
 Definition arg_countType := Eval hnf in [countType of T].
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index baa7231..6f46832 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -255,19 +255,19 @@ Record mixin_of T := Mixin {
 Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.
 Local Coercion base : class_of >->  Equality.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 b bT & phant_id (Equality.class bT) b => Pack (@Class T b m) T.
+  fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m).
 
 (* Inheritance *)
-Definition eqType := @Equality.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
 
 End ClassDef.
 
@@ -408,7 +408,7 @@ Variables (P : pred T) (sT : subType P).
 
 Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT).
 Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin.
-Canonical sub_choiceType := Choice.Pack sub_choiceClass sT.
+Canonical sub_choiceType := Choice.Pack sub_choiceClass.
 
 End SubChoice.
 
@@ -522,19 +522,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 : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
+Structure type : Type := Pack {sort : Type; _ : 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.
 
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 7473ed7..6ed4b97 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -126,14 +126,13 @@ Notation class_of := mixin_of (only parsing).
 
 Section ClassDef.
 
-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 _ := cT return class_of cT in c.
+Definition class := let: Pack _ c := cT return class_of cT in c.
 
-Definition pack c := @Pack T c T.
-Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.
+Definition clone := fun c & cT -> T & phant_id (@Pack T c) cT => Pack c.
 
 End ClassDef.
 
@@ -141,7 +140,7 @@ Module Exports.
 Coercion sort : type >-> Sortclass.
 Notation eqType := type.
 Notation EqMixin := Mixin.
-Notation EqType T m := (@pack T m).
+Notation EqType T m := (@Pack T m).
 Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T)
   (at level 0, format "[ 'eqMixin'  'of'  T ]") : form_scope.
 Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id)
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index d4f564f..8be2eb0 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -172,7 +172,7 @@ Section Mixins.
 Variable T : countType.
 
 Definition EnumMixin :=
-  let: Countable.Pack _ (Countable.Class _ m) _ as cT := T
+  let: Countable.Pack _ (Countable.Class _ m) as cT := T
     return forall e : seq cT, axiom e -> mixin_of cT in
   @Mixin (EqType _ _) m.
 
@@ -198,26 +198,26 @@ Section ClassDef.
 
 Record class_of T := Class {
   base : Choice.class_of T;
-  mixin : mixin_of (Equality.Pack base T)
+  mixin : mixin_of (Equality.Pack base)
 }.
 Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)).
 Local Coercion base : class_of >-> Choice.class_of.
 
-Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type : 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 (EqType T b0)) :=
   fun bT b & phant_id (Choice.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 countType := @Countable.Pack cT (base2 xclass) xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT (base2 xclass).
 
 End ClassDef.
 
@@ -1379,7 +1379,7 @@ Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT).
 Canonical subFinType_subCountType.
 
 Coercion subFinType_finType sT :=
-  Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)) sT.
+  Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)).
 Canonical subFinType_finType.
 
 Lemma codom_val sT x : (x \in codom (val : sT -> T)) = P x.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 1475d55..f30c3a1 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -128,12 +128,9 @@ Notation quot_class_of := quot_mixin_of.
 
 Record quotType := QuotTypePack {
   quot_sort :> Type;
-  quot_class : quot_class_of quot_sort;
-  _ : Type
+  quot_class : quot_class_of quot_sort
 }.
 
-Definition QuotType_pack qT m := @QuotTypePack qT m qT.
-
 Variable qT : quotType.
 Definition pi_phant of phant qT := quot_pi (quot_class qT).
 Local Notation "\pi" := (pi_phant (Phant qT)).
@@ -143,7 +140,7 @@ Lemma repr_ofK : cancel repr_of \pi.
 Proof. by rewrite /pi_phant /repr_of /=; case: qT=> [? []]. Qed.
 
 Definition QuotType_clone (Q : Type) qT cT 
-  of phant_id (quot_class qT) cT := @QuotTypePack Q cT Q.
+  of phant_id (quot_class qT) cT := @QuotTypePack Q cT.
 
 End QuotientDef.
 
@@ -194,7 +191,7 @@ Canonical pi_unlock := Unlockable Pi.E.
 Canonical repr_unlock := Unlockable Repr.E.
 
 Notation quot_class_of := quot_mixin_of.
-Notation QuotType Q m := (@QuotType_pack _ Q m).
+Notation QuotType Q m := (@QuotTypePack _ Q m).
 Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
  (at level 0, format "[ 'quotType'  'of'  Q ]") : form_scope.
 
@@ -329,8 +326,8 @@ Variable eq_quot_op : rel T.
 
 Definition eq_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
   (ec : Equality.class_of Q) :=
-  {mono \pi_(QuotTypePack qc Q) : x y /
-   eq_quot_op x y >-> @eq_op (Equality.Pack ec Q) x y}.
+  {mono \pi_(QuotTypePack qc) : x y /
+   eq_quot_op x y >-> @eq_op (Equality.Pack ec) x y}.
 
 Record eq_quot_class_of (Q : Type) : Type := EqQuotClass {
   eq_quot_quot_class :> quot_class_of T Q;
@@ -341,13 +338,13 @@ Record eq_quot_class_of (Q : Type) : Type := EqQuotClass {
 Record eqQuotType : Type := EqQuotTypePack {
   eq_quot_sort :> Type;
   _ : eq_quot_class_of eq_quot_sort;
-  _ : Type
+ 
 }.
 
 Implicit Type eqT : eqQuotType.
 
 Definition eq_quot_class eqT : eq_quot_class_of eqT :=
-  let: EqQuotTypePack _ cT _ as qT' := eqT return eq_quot_class_of qT' in cT.
+  let: EqQuotTypePack _ cT as qT' := eqT return eq_quot_class_of qT' in cT.
 
 Canonical eqQuotType_eqType eqT := EqType eqT (eq_quot_class eqT).
 Canonical eqQuotType_quotType eqT := QuotType eqT (eq_quot_class eqT).
@@ -358,10 +355,10 @@ Coercion eqQuotType_quotType : eqQuotType >-> quotType.
 Definition EqQuotType_pack Q :=
   fun (qT : quotType T) (eT : eqType) qc ec 
   of phant_id (quot_class qT) qc & phant_id (Equality.class eT) ec => 
-    fun m => EqQuotTypePack (@EqQuotClass Q qc ec m) Q.
+    fun m => EqQuotTypePack (@EqQuotClass Q qc ec m).
 
 Definition EqQuotType_clone (Q : Type) eqT cT 
-  of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT Q.
+  of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT.
 
 Lemma pi_eq_quot eqT : {mono \pi_eqT : x y / eq_quot_op x y >-> x == y}.
 Proof. by case: eqT => [] ? []. Qed.