From 682aa67cc808e1d46b35f6f9c848946cabc226f7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Aug 2014 17:50:29 +0200
Subject: Fixing too restrictive detection of resolution of evars in "apply in"
 (revealed by contribution PTSF).

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

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 0d8bf5560c..71d8d26f15 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -430,3 +430,12 @@ Undo.
 (* H' is displayed as (forall n0, n=n0) *)
 apply H' with (n0:=0).
 Qed.
+
+(* Check that evars originally present in goal do not prevent apply in to work*)
+
+Goal (forall x, x <= 0 -> x = 0) -> exists x, x <= 0 -> 0 = 0.
+intros.
+eexists.
+intros.
+apply H in H0.
+Abort.
-- 
cgit v1.2.3