add some missing test name markers to proofmode_iris

tests/proofmode_iris.ref

@@ -55,6 +55,8 @@
   "Hown" : cinv_own γ p
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
+"test_iInv_2_with_close"
+     : string
 1 goal
   
   Σ : gFunctors
@@ -73,6 +75,8 @@
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
+"test_iInv_4"
+     : string
 1 goal
   
   Σ : gFunctors
@@ -93,6 +97,8 @@
   --------------------------------------∗
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N)) ∗
     (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
+"test_iInv_4_with_close"
+     : string
 1 goal
   
   Σ : gFunctors

tests/proofmode_iris.v

@@ -98,6 +98,7 @@ Section iris_tests.
     iModIntro. iSplit; auto with iFrame.
   Qed.
 
+  Check "test_iInv_2_with_close".
   Lemma test_iInv_2_with_close γ p N P:
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
@@ -116,6 +117,7 @@ Section iris_tests.
     iModIntro. iSplit; auto with iFrame.
   Qed.
 
+  Check "test_iInv_4".
   Lemma test_iInv_4 t N E1 E2 P:
     ↑N ⊆ E2 →
     na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
@@ -126,6 +128,7 @@ Section iris_tests.
     iModIntro. iSplitL "Hown2"; auto with iFrame.
   Qed.
 
+  Check "test_iInv_4_with_close".
   Lemma test_iInv_4_with_close t N E1 E2 P:
     ↑N ⊆ E2 →
     na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2