Remove `_ : Type` from packed classes

This increases performance 10% - 15% for Coq v8.6.1 - v8.9.dev.
Tested on a Debain-based 16-core build server and
a Macbook Pro laptop with 2,3 GHz Intel Core i5.

|                            | Compilation time, old         | Compilation | Speedup |
|                            | (mathcomp commit 967088a6f87) | time, new   |         |
| Coq 8.6.1                  | 10min 33s                     | 9min 10s    | 15%     |
| Coq 8.7.2                  | 10min 12s                     | 8min 50s    | 15%     |
| Coq 8.8.2                  | 9min 39s                      | 8min 32s    | 13%     |
| Coq 8.9.dev(05d827c800544) | 9min 12s                      | 8min 16s    | 11%     |
|                            |                               |             |         |

It seems Coq at some point fixed the problem `_ : Type` was
supposed to solve.

1 files changed, 169 insertions, 171 deletions

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).