From ad55cb4128382852370ea53d36f4d21a83274e8b Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 10 Sep 2020 21:19:55 +0900
Subject: Turn class_of records into primitive records and get rid of the
 xclass idiom

---
 mathcomp/test_suite/test_regular_conv.v | 34 +++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 mathcomp/test_suite/test_regular_conv.v

(limited to 'mathcomp/test_suite')

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.
-- 
cgit v1.2.3