From 3f734c5f5338feb491a6ca021e8b5a578f95c88b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Sep 2017 17:52:34 +0200
Subject: Slightly more straightforward notation for (e)apply.

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

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index a21f3a7f4e..378abb86a8 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -44,6 +44,13 @@ apply &H with (m := 0).
 split.
 Qed.
 
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0.
+Proof.
+intros P H e.
+apply &H with (m := 1) in e.
+exact e.
+Qed.
+
 Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
 Proof.
 intros P H.
-- 
cgit v1.2.3