From 00808a1fa05e34fee36b8dfff4e7c72943b22c23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 18:54:39 +0200
Subject: Short path for Pretyping.ltac_interp_name_env.

Instead of recomputing the evar name environment from scratch when it is
unchanged, we simply return the original one.

This should fix #4964 for good, although I still find the global evar naming
mechanism from Pretyping more than messy. Introducing the heuristic allowing
to capture variables from Ltac in constr binders is indeed the root of many
evils... That is far from being a zero-cost abstraction!
---
 pretyping/pretyping.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ef96e0344..e7f87c5f71 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -403,9 +403,10 @@ let ltac_interp_name_env k0 lvar env =
   (* tail is the part of the env enriched by pretyping *)
   let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
-  let env = pop_rel_context n env in
-  let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
-  push_rel_context ctxt env
+  let open Context.Rel.Declaration in
+  let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+  if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
+  else push_rel_context ctxt' (pop_rel_context n env)
 
 let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
-- 
cgit v1.2.3