From 48249e6831061420ac57f38b538185008f9a5011 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 14 Dec 1999 14:26:48 +0000
Subject: clarification du code

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

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 195b4ce18f..5b0fbe61ca 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -625,7 +625,7 @@ let whd_betadeltaiota_stack env sigma =
       | DOPN(AppL,cl) ->  bdi_rec (array_hd cl)  (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-             | [] -> (x,stack)
+             | [] -> (x,[])
              | (a::m) -> stacklam bdi_rec [a] c m)
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-- 
cgit v1.2.3