[CS] recognize applied primitive projections as keys (fix #9375)

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v
new file mode 100644
index 0000000000..a2bfbafe06
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9375.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Record toto : Type := Toto {
+  toto1 : Type;
+  toto2 : toto1 -> Type
+}.
+
+Record tata := Tata {
+  tata1 : Type
+}.
+
+Canonical Structure tata_toto (x : toto) X :=
+  Tata (toto2 x X).
+
+Check fun (T : toto) (t : toto1 T) =>
+   (eq_refl _ : @tata1 _ = @toto2 _ t).