2 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v
new file mode 100644
index 0000000000..2d5a51345b
--- /dev/null
+++ b/test-suite/success/Case1.v
@@ -0,0 +1,15 @@
+(* Testing eta-expansion of elimination predicate *)
+
+Section NATIND2.
+Variable P : nat -> Type.
+Variable H0 : (P O).
+Variable H1 : (P (S O)).
+Variable H2 : (n:nat)(P n)->(P (S (S n))).
+Fixpoint nat_ind2 [n:nat] : (P n) :=
+         <P>Cases n of  
+                        O     => H0
+                  | (S O)     => H1
+                  | (S (S n)) => (H2 n (nat_ind2 n))
+        end.
+End NATIND2.
+
diff --git a/test-suite/success/Case2.v b/test-suite/success/Case2.v
new file mode 100644
index 0000000000..0aa7b5beff
--- /dev/null
+++ b/test-suite/success/Case2.v
@@ -0,0 +1,11 @@
+(* ============================================== *)
+(*     To test compilation of dependent case      *)
+(*  Nested patterns                               *)
+(* ============================================== *)
+
+Type <[n:nat]n=n>Cases O of 
+                    O => (refl_equal nat O) 
+                  | m => (refl_equal nat m) 
+end.
+
+