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/tacred.mli | |
| 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/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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] *) |