From d55818c7da468ce1c7c9644cb63f68f7561a17bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Sep 2016 13:29:28 +0200
Subject: Tracking careless uses of slow name lookup.

---
 proofs/logic.ml   | 2 +-
 proofs/tacmach.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6f..cc95de646e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -533,7 +533,7 @@ let prim_refiner r sigma goal =
 	      nexthyp,
 	      t,cl,sigma
 	  else
-            (if !check && mem_named_context id (named_context_of_val sign) then
+            (if !check && mem_named_context_val id sign then
 	      errorlabstrm "Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 50984c48e0..ba22db0830 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -191,9 +191,9 @@ module New = struct
     next_ident_away id ids
 
   let pf_get_hyp id gl =
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Proofview.Goal.env gl in
     let sign =
-      try Context.Named.lookup id hyps
+      try Environ.lookup_named id hyps
       with Not_found -> raise (RefinerError (NoSuchHyp id))
     in
     sign
-- 
cgit v1.2.3