diff options
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1784.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 51d5ca728a..718b0e8611 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -93,9 +93,9 @@ Next Obligation. intro H1; contradict H. inversion H1; subst. assumption. contradict H0; assumption. Defined. Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. Defined. -Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. Next Obligation. + intro H1; contradict H. inversion H1; subst. assumption. Defined. +Next Obligation. intro H0; contradict H. inversion H0; subst; auto. Defined. |