Decomposition de Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v
new file mode 100644
index 000000000..73413c475
--- /dev/null
+++ b/test-suite/success/Case10.v
@@ -0,0 +1,26 @@
+(* ============================================== *)
+(*     To test compilation of dependent case      *)
+(*      Multiple Patterns                         *)
+(* ============================================== *)
+Inductive skel: Type :=
+     PROP: skel
+   | PROD: skel->skel->skel.
+
+Parameter Can : skel -> Type.
+Parameter default_can : (s:skel) (Can s).
+
+
+Type [s1,s2:skel]
+      <[s1,_:skel](Can s1)>Cases s1 s2 of
+          PROP PROP => (default_can PROP)
+        | s1 _ => (default_can s1)
+        end.
+
+
+Type [s1,s2:skel]
+<[s1:skel][_:skel](Can s1)>Cases s1 s2 of
+  PROP                 PROP => (default_can PROP)
+| (PROP as s)             _ => (default_can s)
+| ((PROD s1 s2) as s)  PROP => (default_can s)
+| ((PROD s1 s2) as s)   _   => (default_can s)
+end.