From bae29094a5185029dfbd21414a1dccad645d2e32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Jul 2020 17:31:41 +0200
Subject: Fixes reduction effect printing in the presence of non purely
 applicative stacks.

---
 tactics/cbn.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index dfbcc9fbce..8f0966a486 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -571,7 +571,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | None -> fold ())
     | Const (c,u as const) ->
       Reductionops.reduction_effect_hook env sigma c
-         (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
+         (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack)))));
       if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
        let u' = EInstance.kind sigma u in
        match constant_value_in env (c, u') with
-- 
cgit v1.2.3