diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-10 15:23:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-10 15:23:51 +0000 |
| commit | 40011bf94b429432065bcd922932deffa87dcbc0 (patch) | |
| tree | bbde44b7cd30284bb3f5305992f869058b6334a8 /test-suite/bugs/closed | |
| parent | 782372856e836ca106011fada44695c224ae572d (diff) | |
bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made compatible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/closed')
| -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 51d5ca728..718b0e861 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. |