diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1106fefa3..9d6eb31b4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1211,9 +1211,10 @@ let one_step_reduce env sigma c = (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_construct_stack env) sigma fix stack with + (try match reduce_fix (whd_construct_stack env) sigma fix stack with | Reduced s' -> s' - | NotReducible -> raise NotStepReducible) + | NotReducible -> raise NotStepReducible + with Redelimination -> raise NotStepReducible) | _ when isEvalRef env x -> let ref,u = destEvalRefU x in (try |