From 83d1632ed86fbc0ac0a06c0bf2f70adb09c5fb86 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 8 Nov 2019 16:44:34 +0100
Subject: [PATCH] Add test case for `iPoseProof` in embedded logics.

This test case arose in Iron.
---
 tests/proofmode_monpred.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 013a1e199..320355c44 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -193,4 +193,12 @@ Section tests_iprop.
     iMod ("Hclose" with "H2").
     iModIntro. iModIntro. by iNext.
   Qed.
+
+  Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) :
+    x ~~> y → P ∗ ⎡own γ x⎤ ==∗ ⎡own γ y⎤.
+  Proof.
+    iIntros (?) "[_ Hγ]".
+    iPoseProof (own_update with "Hγ") as "H"; first done.
+    by iMod "H".
+  Qed.
 End tests_iprop.
-- 
GitLab