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 /kernel | |
| 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!
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
