diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 13:57:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 13:57:56 +0100 |
| commit | 4ed609a7351882664acd5b5f1525700e7150ce0e (patch) | |
| tree | ca56ce44889e324f8a81def86b1516f3ec838483 /pretyping | |
| parent | f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 (diff) | |
Fixing bug #3916.
Diffstat (limited to 'pretyping')
| -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 |