diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-23 15:40:07 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-23 15:40:07 -0500 |
| commit | eca8e733e15c19ab2e56734f1671f658af690045 (patch) | |
| tree | f0cc23207222dc14161dfe8ed5231ea7d20d7914 /src | |
| parent | fdfeacfad0bba085cb4addd8629ac66a59f123ad (diff) | |
Allow inversion on wff if either side is not a var
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. |