From 02da3f138d5245360cd5e6d510c80bda558b7d9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Dec 2020 12:27:07 +0100
Subject: 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.
---
 pretyping/reductionops.ml | 18 +++++++++---------
 1 file 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
-- 
cgit v1.2.3