Turn class_of records into primitive records and get rid of the xclass idiom

3 files changed, 89 insertions, 89 deletions

diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 2a8dddc..bdff38a 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -125,10 +125,12 @@ Section ClassDef.
 Variable R : ringType.
 Implicit Type phR : phant R.
 
+Set Primitive Projections.
 Record class_of A := Class {
   base1 : GRing.UnitAlgebra.class_of R A;
   mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1)
 }.
+Unset Primitive Projections.
 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.
@@ -138,8 +140,6 @@ 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.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT)
@@ -147,21 +147,21 @@ Definition pack :=
   fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) =>
   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.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition zmodType := @GRing.Zmodule.Pack cT class.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT class.
+Definition ringType := @GRing.Ring.Pack cT class.
+Definition unitRingType := @GRing.UnitRing.Pack cT class.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT class.
+Definition algType := @GRing.Algebra.Pack R phR cT class.
+Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT class.
+Definition vectType := @Vector.Pack R phR cT class.
+Definition vect_ringType := @GRing.Ring.Pack vectType class.
+Definition vect_unitRingType := @GRing.UnitRing.Pack vectType class.
+Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType class.
+Definition vect_algType := @GRing.Algebra.Pack R phR vectType class.
+Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType class.
 
 End ClassDef.
 
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 69c1bb7..df7ef5a 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -93,12 +93,14 @@ Section FieldExt.
 
 Variable R : ringType.
 
+Set Primitive Projections.
 Record class_of T := Class {
   base : Falgebra.class_of R T;
   comm_ext : commutative (Ring.mul base);
   idomain_ext : IntegralDomain.axiom (Ring.Pack base);
   field_ext : Field.mixin_of (UnitRing.Pack base)
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> Falgebra.class_of.
 
@@ -123,8 +125,6 @@ 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.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun (bT : Falgebra.type phR) b
@@ -142,55 +142,55 @@ Definition pack_eta K :=
   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).
 
-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 comAlgType := @ComAlgebra.Pack R phR cT xclass.
-Definition comUnitAlgType := @ComUnitAlgebra.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_comAlgType := @ComAlgebra.Pack R phR FalgType xclass.
-Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR 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_comAlgType := @ComAlgebra.Pack R phR vectType xclass.
-Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType xclass.
-Definition vect_idomainType := @IntegralDomain.Pack vectType xclass.
-Definition vect_fieldType := @Field.Pack vectType xclass.
-
-Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType xclass.
-Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType xclass.
-
-Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass.
-Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass.
-
-Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType xclass.
-Definition comAlg_fieldType := @Field.Pack comAlgType xclass.
-
-Definition alg_idomainType := @IntegralDomain.Pack algType xclass.
-Definition alg_fieldType := @Field.Pack algType xclass.
-
-Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass.
-Definition lalg_fieldType := @Field.Pack lalgType xclass.
-
-Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass.
-Definition lmod_fieldType := @Field.Pack lmodType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition zmodType := @Zmodule.Pack cT class.
+Definition ringType := @Ring.Pack cT class.
+Definition unitRingType := @UnitRing.Pack cT class.
+Definition comRingType := @ComRing.Pack cT class.
+Definition comUnitRingType := @ComUnitRing.Pack cT class.
+Definition idomainType := @IntegralDomain.Pack cT class.
+Definition fieldType := @Field.Pack cT class.
+Definition lmodType := @Lmodule.Pack R phR cT class.
+Definition lalgType := @Lalgebra.Pack R phR cT class.
+Definition algType := @Algebra.Pack R phR cT class.
+Definition unitAlgType := @UnitAlgebra.Pack R phR cT class.
+Definition comAlgType := @ComAlgebra.Pack R phR cT class.
+Definition comUnitAlgType := @ComUnitAlgebra.Pack R phR cT class.
+Definition vectType := @Vector.Pack R phR cT class.
+Definition FalgType := @Falgebra.Pack R phR cT class.
+
+Definition Falg_comRingType := @ComRing.Pack FalgType class.
+Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType class.
+Definition Falg_comAlgType := @ComAlgebra.Pack R phR FalgType class.
+Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR FalgType class.
+Definition Falg_idomainType := @IntegralDomain.Pack FalgType class.
+Definition Falg_fieldType := @Field.Pack FalgType class.
+
+Definition vect_comRingType := @ComRing.Pack vectType class.
+Definition vect_comUnitRingType := @ComUnitRing.Pack vectType class.
+Definition vect_comAlgType := @ComAlgebra.Pack R phR vectType class.
+Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType class.
+Definition vect_idomainType := @IntegralDomain.Pack vectType class.
+Definition vect_fieldType := @Field.Pack vectType class.
+
+Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType class.
+Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType class.
+
+Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType class.
+Definition unitAlg_fieldType := @Field.Pack unitAlgType class.
+
+Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType class.
+Definition comAlg_fieldType := @Field.Pack comAlgType class.
+
+Definition alg_idomainType := @IntegralDomain.Pack algType class.
+Definition alg_fieldType := @Field.Pack algType class.
+
+Definition lalg_idomainType := @IntegralDomain.Pack lalgType class.
+Definition lalg_fieldType := @Field.Pack lalgType class.
+
+Definition lmod_idomainType := @IntegralDomain.Pack lmodType class.
+Definition lmod_fieldType := @Field.Pack lmodType class.
 
 End FieldExt.
 
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index bbd6358..82c4819 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -340,16 +340,16 @@ Variable F : fieldType.
 Definition axiom (L : fieldExtType F) :=
   exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
 
+Set Primitive Projections.
 Record class_of (L : Type) : Type :=
-  Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}.
+  Class {base : FieldExt.class_of F L; mixin : axiom (FieldExt.Pack _ base)}.
+Unset Primitive Projections.
 Local Coercion base : class_of >-> FieldExt.class_of.
 
 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.
-Notation xclass := (class : class_of xT).
 
 Definition clone c of phant_id class c := @Pack phF T c.
 
@@ -357,24 +357,24 @@ 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).
 
-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 comAlgType := @ComAlgebra.Pack F phF cT xclass.
-Definition comUnitAlgType := @ComUnitAlgebra.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.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition zmodType := @Zmodule.Pack cT class.
+Definition ringType := @Ring.Pack cT class.
+Definition unitRingType := @UnitRing.Pack cT class.
+Definition comRingType := @ComRing.Pack cT class.
+Definition comUnitRingType := @ComUnitRing.Pack cT class.
+Definition idomainType := @IntegralDomain.Pack cT class.
+Definition fieldType := @Field.Pack cT class.
+Definition lmodType := @Lmodule.Pack F phF cT class.
+Definition lalgType := @Lalgebra.Pack F phF cT class.
+Definition algType := @Algebra.Pack F phF cT class.
+Definition unitAlgType := @UnitAlgebra.Pack F phF cT class.
+Definition comAlgType := @ComAlgebra.Pack F phF cT class.
+Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT class.
+Definition vectType := @Vector.Pack F phF cT class.
+Definition FalgType := @Falgebra.Pack F phF cT class.
+Definition fieldExtType := @FieldExt.Pack F phF cT class.
 
 End ClassDef.