From ecbeddd188ce513074362678c3fadcbec8d7d5fc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Sep 2017 10:44:15 +0200
Subject: [PATCH] add tests for recently fixed issues

---
 theories/tests/proofmode.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a44213e29..4a3895317 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -181,6 +181,19 @@ Proof.
   iLöb as "IH". iDestruct "IH" as (n) "IH".
   by iExists (S n).
 Qed.
+
+Lemma test_iIntros_start_proof :
+  (True : uPred M)%I.
+Proof.
+  (* Make sure iIntros actually makes progress and enters the proofmode. *)
+  progress iIntros. done.
+Qed.
+
+Lemma test_True_intros : (True : uPred M) -∗ True.
+Proof.
+  iIntros "?". done.
+Qed.
+
 End tests.
 
 Section more_tests.
-- 
GitLab