From 94152ebca87241a509369bb30d01552673603284 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 27 Oct 2020 19:48:28 +0100
Subject: [PATCH] test that view shift notations print

---
 tests/proofmode_iris.ref | 26 ++++++++++++++++++++++++++
 tests/proofmode_iris.v   |  2 ++
 2 files changed, 28 insertions(+)

diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 100a162b6..6e2f09efe 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -28,6 +28,18 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
   
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P
 1 subgoal
   
   Σ : gFunctors
@@ -86,6 +98,20 @@
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
           ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  ============================
+  ↑N ⊆ E2
+  → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
+    ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index e3e510200..a01fafc46 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -101,6 +101,7 @@ Section iris_tests.
   Lemma test_iInv_2 γ p N P:
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
+    Show.
     iIntros "(#?&?)".
     iInv N as "(#HP&Hown)". Show.
     iModIntro. iSplit; auto with iFrame.
@@ -139,6 +140,7 @@ Section iris_tests.
     na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
+    Show.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)" "Hclose". Show.
     iMod ("Hclose" with "[HP Hown2]").
-- 
GitLab