From dc0d370e397d48dbfed36c5bae3882992cd4a31f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 12:12:23 +0000
Subject: [PATCH] Minor tweaks to bupd_plain instance and changelog entry

---
 CHANGELOG.md      | 2 +-
 iris/bi/updates.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 210433e7f..75e7f9ccb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -114,7 +114,7 @@ Coq 8.13 is no longer supported.
   property, a trivial definition of the persistence modality can be given.
 * Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
 * Add `Plain` instance for `|==> P` when `P` is plain.
-  + Rename `bupd_plain` → `bupd_elim`
+* Rename `bupd_plain` → `bupd_elim`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index a75e7762d..964b4567a 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -265,10 +265,10 @@ Section bupd_derived.
         by rewrite (forall_elim x) bupd_elim.
     Qed.
 
-    Global Instance bupd_plain P `{!Plain P} : Plain (|==> P).
+    Global Instance bupd_plain P : Plain P → Plain (|==> P).
     Proof.
-      rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
-      apply plainly_mono, bupd_intro.
+      intros. rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
+      by rewrite -bupd_intro.
     Qed.
 
   End bupd_plainly.
-- 
GitLab