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 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping/cbv.ml')

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) ->
-- 
cgit v1.2.3