From 40011bf94b429432065bcd922932deffa87dcbc0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 10 Feb 2010 15:23:51 +0000 Subject: 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 --- test-suite/bugs/closed/shouldsucceed/1784.v | 4 ++-- 1 file 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 @@ -92,10 +92,10 @@ Next Obligation. intro H; inversion H; subst. Defined. 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. -- cgit v1.2.3