From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 16:30:32 +0200 Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a --- pretyping/reductionops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index fdfa77412..874ea6815 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -134,15 +134,15 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds -> +val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t -val iterate_whd_gen : bool -> Closure.RedFlags.reds -> +val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> Term.constr -> Term.constr (** {6 Generic Optimized Reduction Function using Closures } *) -val clos_norm_flags : Closure.RedFlags.reds -> reduction_function +val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function -- cgit v1.2.3