diff options
| author | herbelin | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /kernel/closure.ml | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
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
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |