From ed623766de468f87c80245dd49cc8b9555d83418 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 18 Jun 2021 15:58:49 +0200
Subject: [PATCH] Fix typos

---
 iris/base_logic/lib/wsat.v | 2 +-
 iris/bi/lib/atomic.v       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index fd6546c97..b2c2f27ce 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 (** All definitions in this file are internal to [fancy_updates] with the
 exception of what's in the [invGS] module. The module [invGS] is thus exported in
-[fancy_updates], which [wsat] is only imported. *)
+[fancy_updates], where [wsat] is only imported. *)
 Module invGS.
   Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
     invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 6e7ddd53b..f67fc975c 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -259,7 +259,7 @@ Section lemmas.
     iApply atomic_acc_mask_weaken. done.
   Qed.
 
-  (** The ellimination form: an atomic accessor *)
+  (** The elimination form: an atomic accessor *)
   Lemma aupd_aacc  Eo Ei α β Φ :
     atomic_update Eo Ei α β Φ -∗
     atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
-- 
GitLab