From b3471b2bf449041b47c19e8e12249e4bb36af3ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 18:06:36 +0200
Subject: Adding more notations for the lulz.

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

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index 95485305dc..a7eb02050b 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -192,3 +192,19 @@ unfold &x at 1.
 let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
 reflexivity.
 Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+exists 0, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+eexists _, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+refine '(let x := 0 in _).
+eexists; exists &x; reflexivity.
+Qed.
-- 
cgit v1.2.3