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.

---
 proofs/logic.ml    | 9 ++++-----
 proofs/logic.mli   | 2 +-
 tactics/tactics.ml | 2 +-
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 613581ade7..285240872e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -230,8 +230,7 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp sigma toleft (left,declfrom,right) hto =
-  let env = Global.env() in
+let move_hyp env sigma toleft (left,declfrom,right) hto =
   let test_dep d d2 =
     if toleft
     then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
@@ -280,11 +279,11 @@ let move_hyp_in_named_context env sigma hfrom hto sign =
   let open EConstr in
   let (left,right,declfrom,toleft) =
     split_sign env sigma hfrom hto (named_context_of_val sign) in
-  move_hyp sigma toleft (left,declfrom,right) hto
+  move_hyp env sigma toleft (left,declfrom,right) hto
 
-let insert_decl_in_named_context sigma decl hto sign =
+let insert_decl_in_named_context env sigma decl hto sign =
   let open EConstr in
-  move_hyp sigma false ([],decl,named_context_of_val sign) hto
+  move_hyp env sigma false ([],decl,named_context_of_val sign) hto
 
 (**********************************************************************)
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9db54732bb..2cad278e10 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -75,6 +75,6 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
 val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
-val insert_decl_in_named_context : Evd.evar_map ->
+val insert_decl_in_named_context : Environ.env -> Evd.evar_map ->
   EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
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