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

1 files changed, 34 insertions, 0 deletions

diff --git a/mathcomp/test_suite/test_regular_conv.v b/mathcomp/test_suite/test_regular_conv.v
new file mode 100644
index 0000000..b6c9f05
--- /dev/null
+++ b/mathcomp/test_suite/test_regular_conv.v
@@ -0,0 +1,34 @@
+From mathcomp Require Import all_ssreflect all_algebra all_field.
+
+Section regular.
+
+Import GRing.
+
+Let eq_ringType_of_regular_lalgType (R : ringType) :=
+  erefl : regular_lalgType R = Ring.Pack (Ring.class R) :> ringType.
+
+Let eq_ringType_of_regular_algType (R : comRingType) :=
+  erefl : regular_algType R = Ring.Pack (Ring.class R) :> ringType.
+
+Let eq_comRingType_of_regular_comAlgType (R : comRingType) :=
+  erefl : regular_comAlgType R = ComRing.Pack (ComRing.class R) :> ringType.
+
+Let eq_unitRingType_of_regular_unitAlgType (R : comUnitRingType) :=
+  erefl : regular_unitAlgType R =
+          UnitRing.Pack (UnitRing.class R) :> unitRingType.
+
+(* The following assertion fails if the class records are not primitive       *)
+(* because the [comUnitAlgType _ of _] packager inserts an eta-expansion on   *)
+(* the class.                                                                 *)
+Let eq_comUnitRingType_of_regular_comUnitAlgType (R : comUnitRingType) :=
+  erefl : regular_comUnitAlgType R =
+          ComUnitRing.Pack (ComUnitRing.class R) :> comUnitRingType.
+
+Let eq_unitRingType_of_regular_FalgType (R : comUnitRingType) :=
+  erefl : regular_FalgType R = UnitRing.Pack (UnitRing.class R) :> unitRingType.
+
+(* The following assertion also fails if the class records are not primitive. *)
+Let eq_fieldType_of_regular_fieldExtType (K : fieldType) :=
+  erefl : regular_fieldExtType K = Field.Pack (Field.class K) :> fieldType.
+
+End regular.