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


From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Oct 2016 13:27:29 +0200
Subject: Quick fix to #4595 (making notations containing "ltac:" unused for
 printing).

Also getting rid of a global side-effect.
---
 pretyping/cases.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e89c3ea719..7e33cc1d4a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2577,6 +2577,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
 	typing_function = typing_fun } in
 
     let j = compile pb in
+
+    (* We coerce to the tycon (if an elim predicate was provided) *)
+    let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
     evdref := !myevdref;
     j in
 
@@ -2587,6 +2590,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
   (* We check for unused patterns *)
   List.iter (check_unused_pattern env) matx;
 
-  (* We coerce to the tycon (if an elim predicate was provided) *)
-  inh_conv_coerce_to_tycon loc env evdref j tycon
-
+  j
-- 
cgit v1.2.3