From 595de46fe3de117129395157dfad28548dc0a157 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 20 Aug 2014 11:13:11 +0200
Subject: An apply test.

---
 test-suite/success/apply.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 29c9ab95ff..48db9c41cf 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -463,6 +463,15 @@ Abort.
 Goal forall H:0=0, H = H.
 intros.
 Fail apply eq_sym in H.
+
+(* Check that unresolved evars not originally present in goal prevent
+   apply in to work*)
+
+Goal (forall x y, x <= 0 -> x + y = 0) -> exists x, x <= 0 -> 0 = 0.
+intros.
+eexists.
+intros.
+Fail apply H in H0.
 Abort.
 
 (* Check naming pattern in apply in *)
-- 
cgit v1.2.3