From 4fabc4b3db8589597ea289e8f93f8bf25445bc9f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 3 Dec 2004 20:25:07 +0000
Subject: Was failing in 8.0pl1

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

diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v
new file mode 100644
index 0000000000..b512b5f820
--- /dev/null
+++ b/test-suite/success/Case8.v
@@ -0,0 +1,7 @@
+(* Check dependencies in the matching predicate (was failing in V8.0pl1) *)
+
+Inductive t : (x:O=O) x=x -> Prop := 
+  c : (x:0=0) (t x (refl_equal ? x)).
+
+Definition a [x:(t ? (refl_equal ? (refl_equal ? O)))] :=
+  <[_;_;x]Cases x of (c y) => Prop end>Cases x of (c y) => y=y end.
-- 
cgit v1.2.3