From 0f7462cc5f8676edaa6b7052edaad40e32fc8234 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Tue, 30 Oct 2018 12:46:11 +0100 Subject: [PATCH] Reduction functions based on CClosure should take an env This is because the env contains typing flags (such as sharing strategy). --- pretyping/tacred.ml | 4 ++-- pretyping/tacred.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8911a2f343e9..4ec8569dd8ae 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c = let cbv_norm_flags flags env sigma t = cbv_norm (create_cbv_infos flags env sigma) t -let cbv_beta = cbv_norm_flags beta empty_env -let cbv_betaiota = cbv_norm_flags betaiota empty_env +let cbv_beta = cbv_norm_flags beta +let cbv_betaiota = cbv_norm_flags betaiota let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma let compute = cbv_betadeltaiota diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index bf38c30a1feb..0887d0efd39f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Call by value strategy (uses Closures) *) val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function - val cbv_beta : local_reduction_function - val cbv_betaiota : local_reduction_function + val cbv_beta : reduction_function + val cbv_betaiota : reduction_function val cbv_betadeltaiota : reduction_function val compute : reduction_function (** = [cbv_betadeltaiota] *)