From 62606e17ff4afe6a897607d45471b7f4d3ef54b8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Nov 2017 11:41:49 +0100
Subject: Binding the specialize tactic.

---
 tests/example2.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index 46e4e43ed0..c953d25061 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -266,3 +266,16 @@ Proof.
 change (?a + 1 = 2) with (2 = $a + 1).
 reflexivity.
 Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl).
+destruct H.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl) as [].
+Qed.
-- 
cgit v1.2.3