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