Merge PR #8689: A few useless accesses to the global environment in pretyping and engine

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9ec3e203cc..18ddc9318d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -451,7 +451,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
-        let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
+        let sign' = insert_decl_in_named_context env sigma (LocalAssum (id,t)) nexthyp sign' in
         sign',t,concl,sigma
       else
         (if check && mem_named_context_val id sign then