diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/WfInversion.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index 4543dce48..4a253f28b 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -142,8 +142,7 @@ End language. Ltac inversion_wff_step := match goal with | [ H : wff _ ?x ?y |- _ ] - => first [ is_var x; fail 1 - | is_var y; fail 1 + => first [ is_var x; is_var y; fail 1 | idtac ]; apply wff_encode in H; unfold wff_code in H; simpl in H end. |