From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

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

(limited to 'test-suite/bugs/closed/shouldsucceed/3000.v')

diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v
new file mode 100644
index 00000000..27de34ed
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3000.v
@@ -0,0 +1,2 @@
+Inductive t (t':Type) : Type := A | B.
+Definition d := match t with _ => 1 end. (* used to fail on list_chop *)
-- 
cgit v1.2.3