From 32fed2acb335b04f55371814d3158637a8373a84 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 22 Aug 2005 11:44:36 +0000
Subject: argument inutilisé de zip: toujours l'identité

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

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index e588ca618c..af00edd65d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -801,23 +801,23 @@ let rec fstrong unfreeze_fun lfts v =
   to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
 *)
 
-let rec zip zfun m stk =
+let rec zip m stk =
   match stk with
     | [] -> m
     | Zapp args :: s ->
         let args = Array.of_list args in
-        zip zfun {norm=neutr m.norm; term=FApp(m, Array.map zfun args)} s
+        zip {norm=neutr m.norm; term=FApp(m, args)} s
     | Zcase(ci,p,br)::s ->
-        let t = FCases(ci, zfun p, m, Array.map zfun br) in
-        zip zfun {norm=neutr m.norm; term=t} s
+        let t = FCases(ci, p, m, br) in
+        zip {norm=neutr m.norm; term=t} s
     | Zfix(fx,par)::s ->
-        zip zfun fx (par @ append_stack_list ([m], s))
+        zip fx (par @ append_stack_list ([m], s))
     | Zshift(n)::s ->
-        zip zfun (lift_fconstr n m) s
+        zip (lift_fconstr n m) s
     | Zupdate(rf)::s ->
-        zip zfun (update rf (m.norm,m.term)) s
+        zip (update rf (m.norm,m.term)) s
 
-let fapp_stack (m,stk) = zip (fun x -> x) m stk
+let fapp_stack (m,stk) = zip m stk
 
 (*********************************************************************)
 
-- 
cgit v1.2.3