diff options
| author | Pierre-Marie Pédrot | 2019-05-06 17:05:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-28 13:07:51 +0200 |
| commit | eabcd5cfe9d96192747d40776668489f9c5e545c (patch) | |
| tree | 1278cf64bce8ec6aa682ca4c4fb8512272d4cdaf /kernel/nativecode.mli | |
| parent | aa52ef99b90ada505d86fea4f4e7d500b9be2433 (diff) | |
Tentative alternative fix for #9992.
We crawl the context in the other direction, preventing the allocation of
the return boolean and enhancing sharing. This fast-path is assuming the
heuristic that the variable being renamed always appears in the context,
otherwise we would be renaming for nothing. It seems to always be the
case, due to the way we pick the set of names to be avoided.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions