*** empty log message ***

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

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v
new file mode 100644
index 000000000..2d5a51345
--- /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.
+