From c53fb4be8c65a89dd03d4aedc2fc65d9807da915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Sep 2017 00:15:09 +0200
Subject: Binding the pose/set family of tactics.

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

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index a7eb02050b..b667e19bbd 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -208,3 +208,17 @@ Proof.
 refine '(let x := 0 in _).
 eexists; exists &x; reflexivity.
 Qed.
+
+Goal True.
+Proof.
+pose (X := True).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+let x := @foo in
+set ($x := True) in * |-.
+constructor.
+Qed.
+
-- 
cgit v1.2.3