From 7bcd56f33a72b9592b1b1030ff3ff10910f2208b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Jun 2018 13:21:10 +0200
Subject: [PATCH] add a test for framing monPred_at below a wand

---
 tests/proofmode_monpred.ref | 11 +++++++++++
 tests/proofmode_monpred.v   |  5 +++++
 2 files changed, 16 insertions(+)

diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 92732da47..8426e3b26 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -35,3 +35,14 @@
   --------------------------------------∗
   ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
   
+1 subgoal
+  
+  I : biIndex
+  PROP : sbi
+  FU0 : BiFUpd PROP * ()
+  P, Q : monpred.monPred I PROP
+  i : I
+  ============================
+  --------------------------------------∗
+  (Q -∗ emp) i
+  
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 3a2c65d60..a61e96470 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -120,7 +120,12 @@ Section tests.
     iIntros "[$ #HP]". iFrame "HP".
   Qed.
 
+  Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
+    P i -∗ (Q -∗ P) i.
+  Proof. iIntros "$". Show. Abort.
+
   Lemma test_iNext_Bi P :
     @bi_entails monPredI (â–· P) (â–· P).
   Proof. iIntros "H". by iNext. Qed.
+
 End tests.
-- 
GitLab