From a59b49b7fe5f41e092609a464ba1df6fba53911f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 26 Mar 2014 13:52:13 +0100
Subject: test for apply + TC resolution

---
 test-suite/success/applyTC.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/success/applyTC.v

diff --git a/test-suite/success/applyTC.v b/test-suite/success/applyTC.v
new file mode 100644
index 0000000000..c2debdecfe
--- /dev/null
+++ b/test-suite/success/applyTC.v
@@ -0,0 +1,15 @@
+Axiom P : nat -> Prop.
+
+Class class (A : Type) := { val : A }.
+
+Lemma usetc {t : class nat} : P (@val nat t).
+Admitted.
+
+Notation "{val:= v }" := (@val _ v).
+
+Instance zero : class nat := {| val := 0 |}.
+
+Lemma test : P 0.
+Fail apply usetc.
+pose (tmp := usetc); apply tmp; clear tmp.
+Qed.
-- 
cgit v1.2.3