From 89c539efe305e0f109b4c612abcbda9daa7bbeea Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 29 Apr 2021 09:13:32 +0000
Subject: [PATCH] Fix typo in the comments.

---
 iris/bi/updates.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 435c788c7..47f9ece52 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -284,7 +284,7 @@ Section fupd_derived.
     ((|={E2,E1}=> emp) ={E2,E3}=∗ P) -∗ |={E1,E3}=> P.
   Proof.
     intros HE.
-    (* Get an [emp] so we can apply [fupd_intro_mask']. *)
+    (* Get an [emp] so we can apply [fupd_mask_subseteq]. *)
     rewrite -[X in (X -∗ _)](left_id emp%I bi_sep).
     rewrite {1}(fupd_mask_subseteq E2) //.
     rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
-- 
GitLab