From 338bac67b6c1111229d90c45875653171bbed4b3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Feb 2018 13:57:06 +0100 Subject: kernel: cleanup projection unfolding - use Redflags.red_projection - share unfold_projection between CClosure and Reduction --- kernel/cClosure.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/cClosure.mli') 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 -- cgit v1.2.3