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 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

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
-- 
cgit v1.2.3