3 files changed, 7 insertions, 26 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 10caf855ba..54a47a252d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -468,23 +468,6 @@ let safe_meta_value sigma ev =
   try Some (Evd.meta_value sigma ev)
   with Not_found -> None
 
-let strong_with_flags whdfun flags env sigma t =
-  let push_rel_check_zeta d env =
-    let open CClosure.RedFlags in
-    let d = match d with
-      | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
-      | d -> d in
-    push_rel d env in
-  let rec strongrec env t =
-    map_constr_with_full_binders env sigma
-      push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
-  strongrec env t
-
-let strong whdfun env sigma t =
-  let rec strongrec env t =
-    map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
-  strongrec env t
-
 (*************************************)
 (*** Reduction using bindingss ***)
 (*************************************)
@@ -1284,7 +1267,9 @@ let plain_instance sigma s c = match s with
 
 let instance env sigma s c =
   (* if s = [] then c else *)
-  strong whd_betaiota env sigma (plain_instance sigma s c)
+  (* No need to compute contexts under binders as whd_betaiota is local *)
+  let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in
+  strongrec (plain_instance sigma s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9d41e7ab58..41d16f1c3c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -143,13 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 type stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
 
-(** {6 Reduction Function Operators } *)
-
-val strong_with_flags :
-  (CClosure.RedFlags.reds -> reduction_function) ->
-  (CClosure.RedFlags.reds -> reduction_function)
-val strong : reduction_function -> reduction_function
-
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1523ec502d..a103699716 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1054,7 +1054,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
 let whd_simpl env sigma c =
   applist (whd_simpl_stack env sigma (c, []))
 
-let simpl env sigma c = strong whd_simpl env sigma c
+let simpl env sigma c =
+  let rec strongrec env t =
+    map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in
+  strongrec env c
 
 (* Reduction at specific subterms *)