From 940da8a791b8b1c704f28662fa2e6a8f3ddf040f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Sep 2017 18:57:18 +0200
Subject: Adding quotations for the assert family of tactics.

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

(limited to 'tests')

diff --git a/tests/example2.v b/tests/example2.v
index 378abb86a8..20819606db 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -222,6 +222,12 @@ pose (X := True).
 constructor.
 Qed.
 
+Goal True.
+Proof.
+pose True as X.
+constructor.
+Qed.
+
 Goal True.
 Proof.
 let x := @foo in
@@ -235,3 +241,22 @@ remember 0 as n eqn: foo at 1.
 rewrite foo.
 reflexivity.
 Qed.
+
+Goal True.
+Proof.
+assert (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+assert (exists n, n = 0) as [n Hn].
++ exists 0; reflexivity.
++ exact I.
+Qed.
+
+Goal True -> True.
+Proof.
+assert (H : 0 + 0 = 0) by reflexivity.
+intros x; exact x.
+Qed.
-- 
cgit v1.2.3