From e9cc023bddc933161a10c71e75ec194b92d2c61a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Mar 2023 15:58:08 +0100
Subject: [PATCH] Add test.

---
 tests/proofmode_iris.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 9915457b0..d1b711e53 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -56,6 +56,11 @@ Section iris_tests.
   Context `{!invGS_gen hlc Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
+  Lemma test_except_0_inv N P : ▷ False -∗ inv N P.
+  Proof.
+    iIntros "H". by iMod "H". (* works because invariants are [IsExcept0] *)
+  Qed.
+
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
-- 
GitLab