diff options
| author | Maxime Dénès | 2018-10-30 12:46:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:10:02 +0100 |
| commit | 0f7462cc5f8676edaa6b7052edaad40e32fc8234 (patch) | |
| tree | b9d59d80058a859d9fbfa0f245e32ccf70ba1d8c /pretyping | |
| parent | 365f14bdb87f6f323d635267f69f507b540ef2a8 (diff) | |
Reduction functions based on CClosure should take an env
This is because the env contains typing flags (such as sharing
strategy).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8911a2f343..4ec8569dd8 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 bf38c30a1f..0887d0efd3 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] *) |