Reduction functions based on CClosure should take an env

This is because the env contains typing flags (such as sharing strategy).
ggonthier · Oct 30, 2018 · 0f7462c · 0f7462c
1 parent 365f14b
commit 0f7462c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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] *)