diff options
| -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] *) |