diff options
| author | Pierre-Marie Pédrot | 2020-08-17 12:57:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-17 12:57:41 +0200 |
| commit | 700aaaacad67d5d5f47805d9aa817213c84cfc02 (patch) | |
| tree | 15d6a1a8b6ed4c233a223168b285bad7dddf5fc3 /pretyping/cbv.ml | |
| parent | ca47fb67a95cf291a43a68b210b9670d4461e9d6 (diff) | |
| parent | bae29094a5185029dfbd21414a1dccad645d2e32 (diff) | |
Merge PR #12751: Fixes reduction effect printing in the presence of non purely applicative stacks
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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) -> |