From 9f005304183ca9c46f6516c08c3c0cc2f1efc05f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Dec 2013 14:04:07 +0100
Subject: Added test-suite for bug #2990.

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

diff --git a/test-suite/bugs/closed/2990.v b/test-suite/bugs/closed/2990.v
new file mode 100644
index 0000000000..5f832626bc
--- /dev/null
+++ b/test-suite/bugs/closed/2990.v
@@ -0,0 +1,8 @@
+Goal True.
+Proof.
+  evar (pfT : Type).
+  cut pfT.
+  subst pfT.
+  intro pf.
+  refine ((fun A : Set => pf A) unit).
+Abort.
-- 
cgit v1.2.3