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

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

(limited to 'proofs/logic.ml')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6..cc95de646 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
-- 
cgit v1.2.3