From 4d060e768ced36ad915daf8e651191a06a802bb3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 20 Mar 2013 17:01:03 +0000
Subject: Check a list length before doing a List.chop (fix #3000)

 I'm not completely sure that raising Not_found is the right
 thing to do here, but it seems reasonable...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16326 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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')

diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v
new file mode 100644
index 0000000000..27de34ed17
--- /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