diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index fd6546c97fb7c3520820d81d560751f6dd932c35..b2c2f27cef10c8965f9266e9891a8f61f8f19a27 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 6e7ddd53b54e02acdfaab72a1391b03db6c31ada..f67fc975c6f8c9046fa3b37f0ab458da5fcbfb7b 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 α β Φ) β Φ.