From 461c9fdd44fea62072a1db312ccfe8472f746203 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 31 May 2021 11:03:55 +0200
Subject: [PATCH] bupd_forall -> bupd_plain_forall

---
 CHANGELOG.md      | 2 ++
 iris/bi/updates.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 923b66e6f..a755c1810 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`.
 * Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` →
   `big_sep{L,L2,M,M2,S}_intro`, and `big_orL_lookup` → `big_orL_intro`.
+* Rename `bupd_forall` to `bupd_plain_forall`.
 
 **Changes in `proofmode`:**
 
@@ -102,6 +103,7 @@ s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 # big_*_intro
 s/\bbig_sep(L|L2|M|M2|S)_intuitionistically_forall\b/big_sep\1_intro/g
 s/\bbig_orL_lookup\b/big_orL_intro/g
+s/\bbupd_forall\b/bupd_plain_forall/g
 EOF
 ```
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 00a97edb9..afeaf0df0 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -230,7 +230,7 @@ Section bupd_derived.
     Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
     Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 
-    Lemma bupd_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
+    Lemma bupd_plain_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
       (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
     Proof.
       apply (anti_symm _).
-- 
GitLab