From 5128f2dc4fddac9f209c3f272cb4353f93f3cb6b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jul 2001 20:29:47 +0000
Subject: Remplacement du tableau du nombre d'args utiles pour la réduction des
 Cases par le nombre d'args inutiles + vérification dans le noyau

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1862 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8523752d29..e56533c51c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -287,8 +287,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
 let reduce_mind_case_use_function (sp,args) env mia =
   match kind_of_term mia.mconstr with 
     | IsMutConstruct(ind_sp,i as cstr_sp, args) ->
-	let ncargs = (fst mia.mci).(i-1) in
-	let real_cargs = list_lastn ncargs mia.mcargs in
+	let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in
 	applist (mia.mlf.(i-1), real_cargs)
     | IsCoFix (_,(names,_,_) as cofix) ->
 	let build_fix_name i =
-- 
cgit v1.2.3