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

Remove `_ : Type` from packed classes

4 files changed, 102 insertions, 102 deletions

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.