diff options
| author | Pierre Letouzey | 2015-12-14 22:31:41 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-14 22:42:29 +0100 |
| commit | ce395ca02311bbe6ecc1b2782e74312272dd15ec (patch) | |
| tree | 5649f9f2b332288a41b23da93411fc064650c81f /kernel/type_errors.ml | |
| parent | 2ab8455cffef4097a441eb6befaa29f6f3076824 (diff) | |
Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
to properly investigate the interaction between all the other optimizations
and MLmagic. But well, at least this precise bug is fixed now.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions