From b6c3f54d04ce441ac68ffabfca69c18847707518 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Aug 2014 17:16:58 +0200
Subject: A reorganization of the "assert" tactics (hopefully uniform naming
 scheme, redundancies, possibility of chaining a tactic knowing the name of
 introduced hypothesis, new proof engine).

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

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 71d8d26f15..57b030fc5d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -439,3 +439,10 @@ eexists.
 intros.
 apply H in H0.
 Abort.
+
+(* Check correct failure of apply in when hypothesis is dependent *)
+
+Goal forall H:0=0, H = H.
+intros.
+Fail apply eq_sym in H.
+Abort.
-- 
cgit v1.2.3