diff options
| author | Pierre-Marie Pédrot | 2018-12-23 15:17:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-23 15:20:28 +0100 |
| commit | 4ea9567b49be0582a5b2420646e5036b60aedd72 (patch) | |
| tree | fae1856e593c7e4c23bbc6ae27486a2a3b0f66fd /kernel/cClosure.mli | |
| parent | b878216ca5e85f8164fa098b9dc0e688a212072d (diff) | |
Remove dead code from CClosure.
It seems that it was a remnant of a time where Reductionops would share the
same data types.
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 |