From bcee0b4d6ca113d225fa7df1cbcfa33812b0bd46 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Mar 2016 18:06:50 +0100
Subject: Test file for #4623.

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

diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v
new file mode 100644
index 0000000000..405d09809c
--- /dev/null
+++ b/test-suite/bugs/4623.v
@@ -0,0 +1,5 @@
+Goal Type -> Type.
+set (T := Type).
+clearbody T.
+refine (@id _).
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3