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/reductionops.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/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index cb84fd8624..aeb18ec322 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -732,7 +732,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 |