From ac461d8032e969a4192430b9c91f2353aa9e7eab Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 2 Jun 2004 15:07:59 +0000
Subject: commentaire

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5789 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/destruct.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index df49928a97..f09863d9d6 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -4,4 +4,6 @@ Parameter f:true=false.
 Goal let p=f in True.
 Intro p.
 LetTac b:=true.
+(* Check that it doesn't fail with an anomaly *)
+(* Ultimately, adapt destruct to make it succeeding *)
 Try NewDestruct b.
-- 
cgit v1.2.3