From bfccb2a29bca36989870aee27b633faa6dc6e6dd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Jul 2021 14:23:41 +0200
Subject: [PATCH] add some missing test name markers to proofmode_iris

---
 tests/proofmode_iris.ref | 6 ++++++
 tests/proofmode_iris.v   | 3 +++
 2 files changed, 9 insertions(+)

diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index f0895eca2..1c66decee 100644
--- a/tests/proofmode_iris.ref
+++ b/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
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 5bfe65ba2..89ac3f556 100644
--- a/tests/proofmode_iris.v
+++ b/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
-- 
GitLab