From 2fac2137bf72662bad76d9baa54611bec8a4143a Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 5 Sep 2001 13:19:12 +0000
Subject: Version de la reduction dans Closure plus econome en memoire: - la
 pile ne contient plus les arguments appliques deja consommes - ajout d'un
 "lock" sur les glacons en cours de calcul

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

(limited to 'kernel/closure.mli')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 6f5afc4e27..e755f28d98 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -134,7 +134,7 @@ val create:
    one by one *)
 
 type 'a stack_member =
-  | Zapp of 'a array * int
+  | Zapp of 'a list
   | Zcase of case_info * 'a * 'a array
   | Zfix of 'a * 'a stack
   | Zshift of int
@@ -182,6 +182,7 @@ type fterm =
   | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
+  | FLOCKED
 
 and freference =
   | FConst of section_path * fconstr array
-- 
cgit v1.2.3