From a5a89e8b623cd5822f59b854a45efc8236ae0087 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 Apr 2019 16:03:06 +0200
Subject: Logic.convert_hyp now takes an environment as an argument.

This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
---
 proofs/logic.ml    | 4 ++--
 proofs/logic.mli   | 2 +-
 tactics/tactics.ml | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index f51f2ea5bc..3fcde56e76 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -548,10 +548,10 @@ and treat_case sigma goal ci lbrty lf acc' =
           (lacc,sigma,fi::bacc))
     (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
 
-let convert_hyp check sign sigma d =
+let convert_hyp ~check env sigma d =
   let id = NamedDecl.get_id d in
   let b = NamedDecl.get_value d in
-  let env = Global.env_of_context sign in
+  let sign = Environ.named_context_val env in
   match lookup_named_ctxt id sign with
   | exception Not_found ->
     if check then error_no_such_hypothesis env sigma id
diff --git a/proofs/logic.mli b/proofs/logic.mli
index f99076db23..163d71f69c 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -62,7 +62,7 @@ type 'id move_location =
 val pr_move_location :
   ('a -> Pp.t) -> 'a move_location -> Pp.t
 
-val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
+val convert_hyp : check:bool -> Environ.env -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
 val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e8869f9b0..5a19f95f90 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -168,7 +168,7 @@ let convert_hyp ?(check=true) d =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let sign = convert_hyp check (named_context_val env) sigma d in
+    let sign = convert_hyp ~check env sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~typecheck:false begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ty
@@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args =
           raise (RefinerError (env, sigma, NoSuchHyp id))
       in
       let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
-      let sign = Logic.convert_hyp check (named_context_val env) sigma d in
+      let sign = Logic.convert_hyp ~check env sigma d in
       let env = reset_with_named_context sign env in
       (env, sigma)
     in
-- 
cgit v1.2.3