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

3 files changed, 201 insertions, 201 deletions

diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index c065cd6..a68ec41 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -254,7 +254,9 @@ Record mixin_of T := Mixin {
   _ : forall P Q : pred T, P =1 Q -> find P =1 find Q
 }.
 
+Set Primitive Projections.
 Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.
+Unset Primitive Projections.
 Local Coercion base : class_of >->  Equality.class_of.
 
 Structure type := Pack {sort; _ : class_of sort}.
@@ -262,14 +264,12 @@ 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.
-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).
 
 (* Inheritance *)
-Definition eqType := @Equality.Pack cT xclass.
+Definition eqType := @Equality.Pack cT class.
 
 End ClassDef.
 
@@ -523,7 +523,9 @@ Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m).
 
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
+Unset Primitive Projections.
 Local Coercion base : class_of >-> Choice.class_of.
 
 Structure type : Type := Pack {sort : Type; _ : class_of sort}.
@@ -531,14 +533,12 @@ 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.
-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).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
 
 End ClassDef.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 7d65f9e..870b797 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -204,10 +204,12 @@ End Mixins.
 
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of T := Class {
   base : Choice.class_of T;
   mixin : mixin_of (Equality.Pack base)
 }.
+Unset Primitive Projections.
 Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)).
 Local Coercion base : class_of >-> Choice.class_of.
 
@@ -216,16 +218,14 @@ 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.
-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).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT (base2 xclass).
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT (base2 class).
 
 End ClassDef.
 
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index e4b956d..b9ed011 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1002,10 +1002,12 @@ Record mixin_of (T0 : Type) (b : Equality.class_of T0)
   _  : transitive    le;
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : Choice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> Choice.class_of.
 
@@ -1018,15 +1020,13 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (Choice.class bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
 End ClassDef.
 
 Module Exports.
@@ -1230,10 +1230,12 @@ Record mixin_of (T0 : Type) (b : POrder.class_of T0)
   _ : forall x y, (x <= y) = (meet x y == x);
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : POrder.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> POrder.class_of.
 
@@ -1246,16 +1248,14 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@POrder.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
 End ClassDef.
 
 Module Exports.
@@ -1341,10 +1341,12 @@ Record mixin_of (T : Type) (b : POrder.class_of T)
   _ : forall x, bottom <= x;
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : Lattice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> Lattice.class_of.
 
@@ -1357,17 +1359,15 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@Lattice.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
 End ClassDef.
 
 Module Exports.
@@ -1444,10 +1444,12 @@ Record mixin_of (T0 : Type) (b : POrder.class_of T0)
   _ : forall x, x <= top;
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : BLattice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> BLattice.class_of.
 
@@ -1460,18 +1462,16 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@BLattice.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
 End ClassDef.
 
 Module Exports.
@@ -1548,10 +1548,12 @@ Record mixin_of (T0 : Type) (b : Lattice.class_of T0)
   _ : @left_distributive T T meet join;
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : Lattice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> Lattice.class_of.
 
@@ -1564,17 +1566,15 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@Lattice.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
 End ClassDef.
 
 Module Exports.
@@ -1613,10 +1613,12 @@ Export DistrLattice.Exports.
 Module BDistrLattice.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : DistrLattice.class_of T;
   mixin : BLattice.mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> DistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : BLattice.class_of T :=
@@ -1629,21 +1631,19 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@DistrLattice.class disp bT) b =>
   fun mT m & phant_id (@BLattice.class disp mT) (BLattice.Class m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition nb_distrLatticeType := @DistrLattice.Pack disp bLatticeType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition nb_distrLatticeType := @DistrLattice.Pack disp bLatticeType class.
 End ClassDef.
 
 Module Exports.
@@ -1674,10 +1674,12 @@ Export BDistrLattice.Exports.
 Module TBDistrLattice.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : BDistrLattice.class_of T;
   mixin : TBLattice.mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> BDistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : TBLattice.class_of T :=
@@ -1690,8 +1692,6 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 : BDistrLattice.class_of T)
@@ -1699,17 +1699,17 @@ Definition pack :=
   fun mT m & phant_id (@TBLattice.class disp mT) (@TBLattice.Class _ b m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
-Definition ntb_distrLatticeType := @DistrLattice.Pack disp tbLatticeType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
+Definition ntb_distrLatticeType := @DistrLattice.Pack disp tbLatticeType class.
 Definition ntb_bDistrLatticeType :=
-  @BDistrLattice.Pack disp tbLatticeType xclass.
+  @BDistrLattice.Pack disp tbLatticeType class.
 End ClassDef.
 
 Module Exports.
@@ -1752,10 +1752,12 @@ Record mixin_of (T0 : Type) (b : BDistrLattice.class_of T0)
   _ : forall x y, (x `&` y) `|` sub x y = x
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : BDistrLattice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> BDistrLattice.class_of.
 
@@ -1768,20 +1770,18 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@BDistrLattice.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
 End ClassDef.
 
 Module Exports.
@@ -1839,11 +1839,13 @@ Record mixin_of (T0 : Type) (b : TBDistrLattice.class_of T0)
   _ : forall x, compl x = sub top x
 }.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : TBDistrLattice.class_of T;
   mixin1 : CBDistrLattice.mixin_of base;
   mixin2 : @mixin_of _ base (CBDistrLattice.sub mixin1);
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> TBDistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : CBDistrLattice.class_of T :=
@@ -1858,27 +1860,25 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c of phant_id class c := @Pack disp T c.
 Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@TBDistrLattice.class disp bT) b =>
   fun mT m0 & phant_id (@CBDistrLattice.class disp mT) (CBDistrLattice.Class m0) =>
   fun m1 => Pack disp (@Class T b m0 m1).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
-Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
-Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass.
-Definition cb_tbLatticeType := @TBLattice.Pack disp cbDistrLatticeType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
+Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class.
+Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT class.
+Definition cb_tbLatticeType := @TBLattice.Pack disp cbDistrLatticeType class.
 Definition cb_tbDistrLatticeType :=
-  @TBDistrLattice.Pack disp cbDistrLatticeType xclass.
+  @TBDistrLattice.Pack disp cbDistrLatticeType class.
 End ClassDef.
 
 Module Exports.
@@ -1947,10 +1947,12 @@ Section ClassDef.
 Definition mixin_of T0 (b : POrder.class_of T0) (T := POrder.Pack tt b) :=
   total (<=%O : rel T).
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : DistrLattice.class_of T;
   mixin : mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> DistrLattice.class_of.
 
@@ -1963,18 +1965,16 @@ Variables (T : Type) (disp : unit) (cT : type disp).
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Definition clone c & phant_id class c := @Pack disp T c.
 Definition clone_with disp' c & phant_id class c := @Pack disp' T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
 
 Definition pack :=
   fun bT b & phant_id (@DistrLattice.class disp bT) b =>
   fun m => Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
 
 End ClassDef.
 
@@ -2016,10 +2016,12 @@ Import Total.Exports.
 Module FinPOrder.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : POrder.class_of T;
   mixin : Finite.mixin_of (Equality.Pack base)
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> POrder.class_of.
 Local Coercion base2 T (c : class_of T) : Finite.class_of T :=
@@ -2032,21 +2034,19 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@POrder.class disp bT) b =>
   fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition count_porderType := @POrder.Pack disp countType xclass.
-Definition fin_porderType := @POrder.Pack disp finType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT class.
+Definition finType := @Finite.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition count_porderType := @POrder.Pack disp countType class.
+Definition fin_porderType := @POrder.Pack disp finType class.
 End ClassDef.
 
 Module Exports.
@@ -2077,10 +2077,12 @@ Bind Scope cpo_sort with FinPOrder.sort.
 Module FinLattice.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base : TBLattice.class_of T;
   mixin : Finite.mixin_of (Equality.Pack base);
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> TBLattice.class_of.
 Local Coercion base2 T (c : class_of T) : FinPOrder.class_of T :=
@@ -2093,32 +2095,30 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@TBLattice.class disp bT) b =>
   fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition count_latticeType := @Lattice.Pack disp countType xclass.
-Definition count_bLatticeType := @BLattice.Pack disp countType xclass.
-Definition count_tbLatticeType := @TBLattice.Pack disp countType xclass.
-Definition fin_latticeType := @Lattice.Pack disp finType xclass.
-Definition fin_bLatticeType := @BLattice.Pack disp finType xclass.
-Definition fin_tbLatticeType := @TBLattice.Pack disp finType xclass.
-Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass.
-Definition finPOrder_bLatticeType := @BLattice.Pack disp finPOrderType xclass.
-Definition finPOrder_tbLatticeType := @TBLattice.Pack disp finPOrderType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT class.
+Definition finType := @Finite.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition finPOrderType := @FinPOrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition count_latticeType := @Lattice.Pack disp countType class.
+Definition count_bLatticeType := @BLattice.Pack disp countType class.
+Definition count_tbLatticeType := @TBLattice.Pack disp countType class.
+Definition fin_latticeType := @Lattice.Pack disp finType class.
+Definition fin_bLatticeType := @BLattice.Pack disp finType class.
+Definition fin_tbLatticeType := @TBLattice.Pack disp finType class.
+Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType class.
+Definition finPOrder_bLatticeType := @BLattice.Pack disp finPOrderType class.
+Definition finPOrder_tbLatticeType := @TBLattice.Pack disp finPOrderType class.
 
 End ClassDef.
 
@@ -2164,10 +2164,12 @@ Export FinLattice.Exports.
 Module FinDistrLattice.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base : TBDistrLattice.class_of T;
   mixin : Finite.mixin_of (Equality.Pack base);
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> TBDistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : FinLattice.class_of T :=
@@ -2180,46 +2182,44 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@TBDistrLattice.class disp bT) b =>
   fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
-Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
-Definition count_distrLatticeType := @DistrLattice.Pack disp countType xclass.
-Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT class.
+Definition finType := @Finite.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition finPOrderType := @FinPOrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition finLatticeType := @FinLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
+Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class.
+Definition count_distrLatticeType := @DistrLattice.Pack disp countType class.
+Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType class.
 Definition count_tbDistrLatticeType :=
-  @TBDistrLattice.Pack disp countType xclass.
-Definition fin_distrLatticeType := @DistrLattice.Pack disp finType xclass.
-Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType xclass.
-Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType xclass.
+  @TBDistrLattice.Pack disp countType class.
+Definition fin_distrLatticeType := @DistrLattice.Pack disp finType class.
+Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType class.
+Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType class.
 Definition finPOrder_distrLatticeType :=
-  @DistrLattice.Pack disp finPOrderType xclass.
+  @DistrLattice.Pack disp finPOrderType class.
 Definition finPOrder_bDistrLatticeType :=
-  @BDistrLattice.Pack disp finPOrderType xclass.
+  @BDistrLattice.Pack disp finPOrderType class.
 Definition finPOrder_tbDistrLatticeType :=
-  @TBDistrLattice.Pack disp finPOrderType xclass.
+  @TBDistrLattice.Pack disp finPOrderType class.
 Definition finLattice_distrLatticeType :=
-  @DistrLattice.Pack disp finLatticeType xclass.
+  @DistrLattice.Pack disp finLatticeType class.
 Definition finLattice_bDistrLatticeType :=
-  @BDistrLattice.Pack disp finLatticeType xclass.
+  @BDistrLattice.Pack disp finLatticeType class.
 Definition finLattice_tbDistrLatticeType :=
-  @TBDistrLattice.Pack disp finLatticeType xclass.
+  @TBDistrLattice.Pack disp finLatticeType class.
 
 End ClassDef.
 
@@ -2276,10 +2276,12 @@ Export FinDistrLattice.Exports.
 Module FinCDistrLattice.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : CTBDistrLattice.class_of T;
   mixin : Finite.mixin_of (Equality.Pack base);
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> CTBDistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : FinDistrLattice.class_of T :=
@@ -2292,48 +2294,46 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@CTBDistrLattice.class disp bT) b =>
   fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
-Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
-Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass.
-Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass.
-Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT class.
+Definition finType := @Finite.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition finPOrderType := @FinPOrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition finLatticeType := @FinLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
+Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class.
+Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT class.
+Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT class.
+Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT class.
 Definition count_cbDistrLatticeType :=
-  @CBDistrLattice.Pack disp countType xclass.
+  @CBDistrLattice.Pack disp countType class.
 Definition count_ctbDistrLatticeType :=
-  @CTBDistrLattice.Pack disp countType xclass.
-Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType xclass.
-Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType xclass.
+  @CTBDistrLattice.Pack disp countType class.
+Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType class.
+Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType class.
 Definition finPOrder_cbDistrLatticeType :=
-  @CBDistrLattice.Pack disp finPOrderType xclass.
+  @CBDistrLattice.Pack disp finPOrderType class.
 Definition finPOrder_ctbDistrLatticeType :=
-  @CTBDistrLattice.Pack disp finPOrderType xclass.
+  @CTBDistrLattice.Pack disp finPOrderType class.
 Definition finLattice_cbDistrLatticeType :=
-  @CBDistrLattice.Pack disp finLatticeType xclass.
+  @CBDistrLattice.Pack disp finLatticeType class.
 Definition finLattice_ctbDistrLatticeType :=
-  @CTBDistrLattice.Pack disp finLatticeType xclass.
+  @CTBDistrLattice.Pack disp finLatticeType class.
 Definition finDistrLattice_cbDistrLatticeType :=
-  @CBDistrLattice.Pack disp finDistrLatticeType xclass.
+  @CBDistrLattice.Pack disp finDistrLatticeType class.
 Definition finDistrLattice_ctbDistrLatticeType :=
-  @CTBDistrLattice.Pack disp finDistrLatticeType xclass.
+  @CTBDistrLattice.Pack disp finDistrLatticeType class.
 
 End ClassDef.
 
@@ -2394,10 +2394,12 @@ Export FinCDistrLattice.Exports.
 Module FinTotal.
 Section ClassDef.
 
+Set Primitive Projections.
 Record class_of (T : Type) := Class {
   base  : FinDistrLattice.class_of T;
   mixin : Total.mixin_of base;
 }.
+Unset Primitive Projections.
 
 Local Coercion base : class_of >-> FinDistrLattice.class_of.
 Local Coercion base2 T (c : class_of T) : Total.class_of T :=
@@ -2410,40 +2412,38 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 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 (@FinDistrLattice.class disp bT) b =>
   fun mT m & phant_id (@Total.class disp mT) (Total.Class m) =>
   Pack disp (@Class T b m).
 
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition bLatticeType := @BLattice.Pack disp cT xclass.
-Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
-Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
-Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
-Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
-Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass.
-Definition orderType := @Total.Pack disp cT xclass.
-Definition order_countType := @Countable.Pack orderType xclass.
-Definition order_finType := @Finite.Pack orderType xclass.
-Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass.
-Definition order_bLatticeType := @BLattice.Pack disp orderType xclass.
-Definition order_tbLatticeType := @TBLattice.Pack disp orderType xclass.
-Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass.
-Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType xclass.
+Definition eqType := @Equality.Pack cT class.
+Definition choiceType := @Choice.Pack cT class.
+Definition countType := @Countable.Pack cT class.
+Definition finType := @Finite.Pack cT class.
+Definition porderType := @POrder.Pack disp cT class.
+Definition finPOrderType := @FinPOrder.Pack disp cT class.
+Definition latticeType := @Lattice.Pack disp cT class.
+Definition bLatticeType := @BLattice.Pack disp cT class.
+Definition tbLatticeType := @TBLattice.Pack disp cT class.
+Definition finLatticeType := @FinLattice.Pack disp cT class.
+Definition distrLatticeType := @DistrLattice.Pack disp cT class.
+Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class.
+Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class.
+Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT class.
+Definition orderType := @Total.Pack disp cT class.
+Definition order_countType := @Countable.Pack orderType class.
+Definition order_finType := @Finite.Pack orderType class.
+Definition order_finPOrderType := @FinPOrder.Pack disp orderType class.
+Definition order_bLatticeType := @BLattice.Pack disp orderType class.
+Definition order_tbLatticeType := @TBLattice.Pack disp orderType class.
+Definition order_finLatticeType := @FinLattice.Pack disp orderType class.
+Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType class.
 Definition order_tbDistrLatticeType :=
-  @TBDistrLattice.Pack disp orderType xclass.
+  @TBDistrLattice.Pack disp orderType class.
 Definition order_finDistrLatticeType :=
-  @FinDistrLattice.Pack disp orderType xclass.
+  @FinDistrLattice.Pack disp orderType class.
 
 End ClassDef.