diff options
| author | Pierre-Marie Pédrot | 2020-12-18 12:27:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:03:02 +0100 |
| commit | 02da3f138d5245360cd5e6d510c80bda558b7d9b (patch) | |
| tree | 268fc6b8c174bfd3d9040efd0a07b7e984cfec93 /kernel/vmlambda.ml | |
| parent | 90c0d4e66acd8114f77e90aca4549a003a0c4626 (diff) | |
Try to preserve the old unification behaviour w.r.t. let-ins in branches.
The infamous whd_betaiota_deltazeta_for_iota_state function is critical for
unification, and it seems that eagerly reducing let-bindings appearing in
case branches was a bad idea for efficiency. Instead, when try to preserve
the old behaviour where a dummy beta-let cut was introduced.
Diffstat (limited to 'kernel/vmlambda.ml')
0 files changed, 0 insertions, 0 deletions