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.

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

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6d80db6455..36353653a7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let x = id_of_name_using_hdchar (Global.env()) t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
-    if mem_named_context x (named_context env) then
+    if mem_named_context_val x (named_context_val env) then
       errorlabstrm "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
-- 
cgit v1.2.3