From d755c546a5c260232fd30971bd604b078d0afc18 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 17:31:13 +0200
Subject: Properly implementing the notation to easily access hypotheses.

---
 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 398f33561e..ca9e3dcff5 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -19,3 +19,10 @@ Proof.
 let myvar := Std.NamedHyp @x in split with (?myvar := 0).
 split.
 Qed.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+intros H.
+elim &H with 0.
+split.
+Qed.
-- 
cgit v1.2.3