From a9fb1b03f50b7ac2d5a273b44f64ce49bc42db60 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 22 Jan 2019 10:39:50 +0100
Subject: [CS] recognize applied primitive projections as keys (fix #9375)

---
 test-suite/bugs/closed/bug_9375.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9375.v

(limited to 'test-suite')

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