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

1 files changed, 9 insertions, 1 deletions

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