From 405a80db00537b5ccfb3b8655cd7baf61e890b20 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 19:47:41 +0200
Subject: Passing env functionally in move_hyp and
 insert_decl_in_named_context.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3