diff options
| author | Pierre-Marie Pédrot | 2016-08-21 18:54:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-21 19:21:00 +0200 |
| commit | 00808a1fa05e34fee36b8dfff4e7c72943b22c23 (patch) | |
| tree | fe84fd14a444f639d336a4184ebbca9e5118ac55 | |
| parent | 6278ce16ab1b8b65c7d1770d265471f594c8e793 (diff) | |
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!
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files 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 |