test that view shift notations print

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

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]").