diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 13:57:06 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 14:41:23 +0100 |
| commit | 338bac67b6c1111229d90c45875653171bbed4b3 (patch) | |
| tree | 27fbf43fbbceeccf077cf8ad7718c082bbffbbf2 /kernel/cClosure.mli | |
| parent | 76aff3cbe39da657abb1f559b8ba411a49aab317 (diff) | |
kernel: cleanup projection unfolding
- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 119b70e30..bf214ae24 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -163,6 +163,7 @@ 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 +val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use |