diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/cbn.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |