From 4d2df571b3f1246a85961e20d37b24913a92ec57 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Thu, 17 Jun 2021 10:35:52 +0000
Subject: [PATCH] Apply 4 suggestion(s) to 1 file(s)

---
 iris/bi/lib/atomic.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index b71edf02c..5c3c3c61f 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -444,10 +444,10 @@ Section proof_mode.
   Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
 
   (** We'd like to use the [iModIntro] machinery to transform the context into
-  smoething all-laterable, but we cannot actually use [iModIntro] on
-  [make_laterable]for that since we need to first make the context laterable,
+  something all-laterable, but we cannot actually use [iModIntro] on
+  [make_laterable] for that since we need to first make the context laterable,
   then apply coinduction, and then introduce the modality (the last two steps
-  happen inside [aupd_intro]). We instead we define a dummy modality that also
+  happen inside [aupd_intro]). We instead we define a dummy modality [make_laterable_id] that also
   uses [MIEnvTransform IntoLaterable] and use that to pre-process the goal. *)
   Local Definition make_laterable_id (P : PROP) := P.
 
@@ -469,7 +469,7 @@ Section proof_mode.
     make_laterable_id P -∗ P.
   Proof. done. Qed.
 
-  (** We need PROP to be affine as otherwise [emp] is not [Laterable]. *)
+  (** We need [PROP] to be affine as otherwise [emp] is not [Laterable]. *)
   Lemma tac_aupd_intro `{!BiAffine PROP} Γp Γs n α β Eo Ei Φ P :
     TCForall Laterable (env_to_list Γs) →
     P = env_to_prop Γs →
-- 
GitLab