diff options
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4576.v | 3 |
2 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 13b7fb4079..7c7b31395e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -811,7 +811,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let fold () = let () = if !debug_RAKAM then let open Pp in pp (str "<><><><><>" ++ fnl ()) in - if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l) + (s,cst_l) in match kind_of_term x with | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> @@ -1002,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in - whrec (Option.default Cst_stack.empty csts) + fun xs -> + let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in + if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res (** reduction machine without global env and refold machinery *) let local_whd_state_gen flags sigma = diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v new file mode 100644 index 0000000000..2c643ea779 --- /dev/null +++ b/test-suite/bugs/closed/4576.v @@ -0,0 +1,3 @@ +Definition foo := O. +Arguments foo : simpl nomatch. +Timeout 1 Eval cbn in id foo. |