diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 119b70e301..c43fc46239 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -61,6 +61,9 @@ module type RedFlagsSig = sig (** Adds a reduction kind to a set *) val red_add_transparent : reds -> transparent_state -> reds + (** Retrieve the transparent state of the reduction flags *) + val red_transparent : reds -> transparent_state + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds @@ -163,6 +166,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 |