From 3478ffda0a0a83951db341eb68fc6b71877c1392 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 28 Apr 2008 09:27:17 +0000
Subject: Backtrack on using metas eagerly in auto, only done in "new auto" for
 now. Fix proof scripts that failed correspondingly. Should make many contribs
 compile again...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/1784.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index d6b7660b2d..616dd26f5d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -85,7 +85,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
       end
   end.
 
-Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined.
+Next Obligation. apply H; inversion H0; subst; trivial. Defined.
 Next Obligation. inversion H. Defined.
 Next Obligation. inversion H. Defined.
 Next Obligation. inversion H; subst. Defined.
-- 
cgit v1.2.3