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.

---
 pretyping/cbv.ml          | 6 +++++-
 pretyping/reductionops.ml | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2c7b689c04..2661000a39 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -397,6 +397,10 @@ and apply_env env t =
   | _ ->
     map_with_binders subs_lift apply_env env t
 
+let rec strip_app = function
+  | APP (args,st) -> APP (args,strip_app st)
+  | s -> TOP
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack),
@@ -442,7 +446,7 @@ let rec norm_head info env t stack =
 
   | Const sp ->
     Reductionops.reduction_effect_hook info.env info.sigma
-      (fst sp) (lazy (reify_stack t stack));
+      (fst sp) (lazy (reify_stack t (strip_app stack)));
     norm_head_ref 0 info env stack (ConstKey sp) t
 
   | LetIn (_, b, _, c) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fdc770dba6..bbd8fa0434 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -757,7 +757,7 @@ let rec whd_state_gen flags env sigma =
       | None -> fold ())
     | Const (c,u as const) ->
       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