From 4849c8eb1b7a386d2abcbc80c40de34b0a69b8ea Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Mar 2016 18:18:54 +0100
Subject: Test file for #4624, fixed by Matthieu's bfce815bd1.

---
 test-suite/bugs/4624.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/4624.v

diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v
new file mode 100644
index 0000000000..a737afcdab
--- /dev/null
+++ b/test-suite/bugs/4624.v
@@ -0,0 +1,7 @@
+Record foo := mkfoo { type : Type }.
+
+Canonical Structure fooA (T : Type) := mkfoo (T -> T).
+
+Definition id (t : foo) (x : type t) := x.
+
+Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file
-- 
cgit v1.2.3