From 50b20a3076c5c8dfe4cf77ccfa65f33c873a2fab Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 Sep 2014 10:29:25 +0200
Subject: Fixing injection bug #3616 on sigma-types.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3616.v b/test-suite/bugs/closed/3616.v
new file mode 100644
index 0000000000..688700260c
--- /dev/null
+++ b/test-suite/bugs/closed/3616.v
@@ -0,0 +1,3 @@
+(* Was failing from April 2014 to September 2014 because of injection *)
+Goal forall P e es t, (e :: es = existT P tt t :: es)%list -> True.
+inversion 1.
-- 
cgit v1.2.3