From 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Sep 2000 11:02:30 +0000
Subject: Modification mkAppL; abstraction via kind_of_term; changement dans
 Reduction

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

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 178e5a9de7..783017e8a4 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -395,8 +395,8 @@ let rec norm_head info env t stack =
   (* stack grows (remove casts) *)
   | IsAppL (head,args) -> (* Applied terms are normalized immediately;
                         they could be computed when getting out of the stack *)
-      let nargs = List.map (cbv_stack_term info TOP env) args in
-      norm_head info env head (stack_app nargs stack)
+      let nargs = Array.map (cbv_stack_term info TOP env) args in
+      norm_head info env head (stack_app (Array.to_list nargs) stack)
   | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
   | IsCast (ct,_) -> norm_head info env ct stack
 
-- 
cgit v1.2.3