From d5b8d356ca0441dc96b87bd7615147813d7aa64a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 May 2006 22:32:33 +0000
Subject: Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la
 casse

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8884 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Destruct.v | 13 -------------
 test-suite/success/destruct.v | 16 ++++++++++++++++
 2 files changed, 16 insertions(+), 13 deletions(-)
 delete mode 100644 test-suite/success/Destruct.v

diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v
deleted file mode 100644
index b909e45e72..0000000000
--- a/test-suite/success/Destruct.v
+++ /dev/null
@@ -1,13 +0,0 @@
-(* Submitted by Robert Schneck *)
-
-Parameter A B C D : Prop.
-Axiom X : A -> B -> C /\ D.
-
-Lemma foo : A -> B -> C.
-Proof.
-intros. 
-destruct X. (* Should find axiom X and should handle arguments of X *)
-assumption.
-assumption.
-assumption.
-Qed.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index ede573a34e..9f938e10f4 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,3 +1,17 @@
+(* Submitted by Robert Schneck *)
+
+Parameter A B C D : Prop.
+Axiom X : A -> B -> C /\ D.
+
+Lemma foo : A -> B -> C.
+Proof.
+intros. 
+destruct X. (* Should find axiom X and should handle arguments of X *)
+assumption.
+assumption.
+assumption.
+Qed.
+
 (* Simplification of bug 711 *)
 
 Parameter f : true = false.
@@ -7,3 +21,5 @@ set (b := true) in *.
 (* Check that it doesn't fail with an anomaly *)
 (* Ultimately, adapt destruct to make it succeeding *)
 try destruct b.
+Abort.
+
-- 
cgit v1.2.3