diff options
| author | Gaëtan Gilbert | 2019-04-08 16:00:53 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-08 16:00:53 +0200 |
| commit | e9738ee2d21a84fc946d168aeaa68b169b309fd8 (patch) | |
| tree | b4b30d32deb6255b16b750db6459533618e3f7e6 /kernel/nativelib.mli | |
| parent | 70a00b72035be1f5c3900a78df97d7350cc70bb6 (diff) | |
Don't store closures in summary (reduction effects)
We already have indirection (constant -> effect name, effect name ->
function) so we only need to stop using summary.ref for the second map.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions