From b5767192ebc85ca609a45f8fa3b77b9305ddcc98 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Mar 2018 19:16:48 +0100
Subject: [PATCH] add a test for 'done' not to loop

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 45c124d98..b6b108929 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -416,4 +416,7 @@ Proof.
   - reflexivity.
 Qed.
 
+Lemma test_iAssumption_False_no_loop : âˆƒ R, R âŠ¢ âˆ€ P, P.
+Proof. eexists. iIntros "?" (P). done. Qed.
+
 End tests.
-- 
GitLab