diff options
Diffstat (limited to 'src/Reflection/InlineCastWf.v')
| -rw-r--r-- | src/Reflection/InlineCastWf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/InlineCastWf.v b/src/Reflection/InlineCastWf.v index 9f5b0b348..c973335d0 100644 --- a/src/Reflection/InlineCastWf.v +++ b/src/Reflection/InlineCastWf.v @@ -69,7 +69,7 @@ Section language. | [ H : forall e, Some _ = Some e -> _ |- _ ] => specialize (H _ eq_refl) | _ => solve [ auto with wf ] - | _ => progress inversion_wff_constr + | _ => progress inversion_wf_constr | _ => progress inversion_flat_type | [ H : context[match ?e with _ => _ end] |- _ ] => invert_one_expr e | [ |- context[match ?e with _ => _ end] ] => invert_one_expr e |