diff options
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7ec56e3ade..0240cdbc25 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -125,8 +125,8 @@ let special_red_case env whfun p c ci lf = raise Redelimination | _ -> if reducible_mind_case constr then - reduce_mind_case env - {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf} + reduce_mind_case + {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf} else raise Redelimination in |