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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 874457ae52..3da75f67b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -713,15 +713,15 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = let args = Stack.tail ci.ci_npar args in let args = Option.get (Stack.list_of_app_stack args) in let br = lf.(i - 1) in - let subst = - if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then - (* No let-bindings *) - List.rev args - else - let ctx = expand_branch env sigma u pms (ind, i) br in - subst_of_rel_context_instance ctx args - in - Vars.substl subst (snd br) + if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then + (* No let-bindings *) + let subst = List.rev args in + Vars.substl subst (snd br) + else + (* For backwards compat with unification, we do not reduce the let-bindings + upfront. *) + let ctx = expand_branch env sigma u pms (ind, i) br in + applist (it_mkLambda_or_LetIn (snd br) ctx, args) let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in |