1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v
new file mode 100644
index 00000000..08078012
--- /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.
+