From fae106f740d3d71555933cf416eec905c58f417e Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 23 Mar 2001 15:04:09 +0000
Subject: amelioration de la consommation memoire de la conversion en
 eta-expansant les definitions.

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

(limited to 'kernel/closure.mli')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index ef01b73bb1..b8d40152a6 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -106,7 +106,15 @@ val create:
    [append_stack] one array at a time but popped with [decomp_stack]
    one by one *)
 
-type 'a stack
+type 'a stack_member =
+  | Zapp of 'a array * int
+  | Zcase of case_info * 'a * 'a array
+  | Zfix of 'a * 'a stack
+  | Zshift of int
+  | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
 val empty_stack : 'a stack
 val append_stack : 'a array -> 'a stack -> 'a stack
 
-- 
cgit v1.2.3