diff options
| author | Maxime Dénès | 2019-01-02 23:37:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-02 23:37:18 +0100 |
| commit | 0a5bbf347b5bbcb579f94eb3d0166778cd92cfdb (patch) | |
| tree | 9b98314ee135c924cf132a2c50c5e9443ef95ef0 /kernel/cClosure.mli | |
| parent | 2760bdc584d3b49d9ebcd2052c6be13e08cb1429 (diff) | |
| parent | 4ea9567b49be0582a5b2420646e5036b60aedd72 (diff) | |
Merge PR #9276: Remove dead code from CClosure.
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c2d53eed47..46be1bb279 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -123,8 +123,7 @@ type fterm = (*********************************************************************** s A [stack] is a context of arguments, arguments are pushed by - [append_stack] one array at a time but popped with [decomp_stack] - one by one *) + [append_stack] one array at a time *) type stack_member = | Zapp of fconstr array @@ -139,13 +138,7 @@ and stack = stack_member list val empty_stack : stack val append_stack : fconstr array -> stack -> stack -val decomp_stack : stack -> (fconstr * stack) option -val array_of_stack : stack -> fconstr array -val stack_assign : stack -> int -> fconstr -> stack val stack_args_size : stack -> int -val stack_tail : int -> stack -> stack -val stack_nth : stack -> int -> fconstr -val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack (** To lazy reduce a constr, create a [clos_infos] with |