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
---
 pretyping/inductiveops.ml                   | 1 +
 test-suite/bugs/closed/shouldsucceed/3000.v | 2 ++
 2 files changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/3000.v

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 0017fee788..ef95fbb5c8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -327,6 +327,7 @@ let find_rectype env sigma c =
   match kind_of_term t with
     | Ind ind ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
+        if mib.mind_nparams > List.length l then raise Not_found;
         let (par,rargs) = List.chop mib.mind_nparams l in
         IndType((ind, par),rargs)
     | _ -> raise Not_found
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