From 99860bb8fc9d2cf7b750bb6c8acdfa8c43431a3e Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 10 May 2006 20:47:28 +0000
Subject: correction bugs dans Cbv (beta n-aire)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8802 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ff456b93ce..6bdca4f8ff 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -882,7 +882,7 @@ let rec get_args n tys f e stk =
           let eargs = Array.sub l n (na-n) in
           (Inl (subs_cons(args,e)), Zapp eargs :: s)
         else (* more lambdas *)
-          let (_,etys) = list_chop na tys in
+          let etys = list_skipn na tys in
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
-- 
cgit v1.2.3