test for apply + TC resolution

1 files changed, 15 insertions, 0 deletions

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.