From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 18:47:45 +0200
Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v
new file mode 100644
index 0000000000..9a35bcf954
--- /dev/null
+++ b/test-suite/bugs/closed/4893.v
@@ -0,0 +1,4 @@
+Goal True.
+evar (P: Prop).
+assert (H : P); [|subst P]; [exact I|].
+let T := type of H in not_evar T.
-- 
cgit v1.2.3