From c515a8acb4acbe7e73121f1060ffef31d96a1436 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Aug 2017 17:14:38 +0200
Subject: Adding a notation for the unfold tactic.

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

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index af664ef163..6b26b78022 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -182,3 +182,11 @@ Proof.
 lazy.
 reflexivity.
 Qed.
+
+Goal let x := 1 + 1 - 1 in x = x.
+Proof.
+intros x.
+unfold &x at 1.
+let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
+reflexivity.
+Qed.
-- 
cgit v1.2.3