aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-08-21 18:54:39 +0200
committerPierre-Marie Pédrot2016-08-21 19:21:00 +0200
commit00808a1fa05e34fee36b8dfff4e7c72943b22c23 (patch)
treefe84fd14a444f639d336a4184ebbca9e5118ac55 /kernel
parent6278ce16ab1b8b65c7d1770d265471f594c8e793 (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!
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions