From 8b9ef591524c32ce773fd22874adaa190227f3c8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 May 2011 15:37:02 +0000
Subject: Mini-test for eta

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

diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v
new file mode 100644
index 0000000000..08078012a9
--- /dev/null
+++ b/test-suite/success/eta.v
@@ -0,0 +1,19 @@
+(* Kernel test (head term is a constant) *)
+Check (fun a : S = S => a : S = fun x => S x).
+
+(* Kernel test (head term is a variable) *)
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
+
+(* Test type inference  (head term is syntactically rigid) *)
+Check (fun (a : list = list) => a : list = fun A => _ A).
+
+(* Test type inference (head term is a variable) *)
+(* This one is still to be done...
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
+*)
+
+(* Test tactic unification *)
+Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
+intro H; apply H.
+Qed.
+
-- 
cgit v1.2.3