diff options
| author | Pierre-Marie Pédrot | 2021-01-06 16:29:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-18 13:36:46 +0100 |
| commit | a47e7822338bf0d2ab21c1f9a3b8bfef7a9b50b4 (patch) | |
| tree | 9d9e2b4625dccf3bc424b0e7de594c47c668cdbc /kernel | |
| parent | 875e410294503b03f0954c94164bd611a5682850 (diff) | |
Do not call the with_full_binder map variant for Reduction.instance.
We know statically that whd_betaiota is a local reduction function, so it
does not need to access the rel_context of its environment argument.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
