diff options
| author | Pierre-Marie Pédrot | 2019-05-04 19:50:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-28 13:07:51 +0200 |
| commit | aa52ef99b90ada505d86fea4f4e7d500b9be2433 (patch) | |
| tree | c341bc72dee32765686360f2f68a21f2ab8c5dda /plugins/syntax | |
| parent | e005f390312b8900df36aa27bc087e18701c8fcd (diff) | |
Faster renaming of shadowed variables in evar instance creation.
Instead of blindly renaming the variables in all the terms in the context,
we only do so for those appearing after the variable being renamed. By
typing, we know that the other ones cannot refer to the variable being
replaced.
Fixes #9992.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions