diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 10 |
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 |