Adding quotations for the assert family of tactics.

1 files changed, 25 insertions, 0 deletions

diff --git a/tests/example2.v b/tests/example2.v
index 378abb86a8..20819606db 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -224,6 +224,12 @@ Qed.
 
 Goal True.
 Proof.
+pose True as X.
+constructor.
+Qed.
+
+Goal True.
+Proof.
 let x := @foo in
 set ($x := True) in * |-.
 constructor.
@@ -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.