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, 53 insertions, 53 deletions

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.