diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1e91b7250e6ef918f0be1e5d4e6ab089530f1c7b..e2dfa3d07078000a5a140de34939177711f85a54 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -406,7 +406,7 @@ Spies, and Tej Chajed.  Thanks a lot to everyone involved!
 * Make lemma `Excl_included` a bi-implication.
 * Make `auth_update_core_id` work with any fraction of the authoritative
   element.
-* Add `min_nat`, a RA for natural numbers with `min` as the operation.
+* Add `min_nat`, an RA for natural numbers with `min` as the operation.
 * Add many missing `Proper`/non-expansiveness lemmas for maps and lists.
 * Add `list_singletonM_included` and `list_lookup_singletonM_{lt,gt}` lemmas
   about singletons in the list RA.
diff --git a/tex/derived.tex b/tex/derived.tex
index 119a24fa98d56d4b5e51ba07e10192fc269264f0..24b5e7d4a910e20d6b91eb0cb97737a66d414d64 100644
--- a/tex/derived.tex
+++ b/tex/derived.tex
@@ -91,11 +91,11 @@ from which we can derive
 
 \subsection{Boxes}
 
-The idea behind the \emph{boxes} is to have an proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
+The idea behind the \emph{boxes} is to have a proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
 In some sense, this is a replacement for having an ``authoritative PCM of Iris propositions itself''.
 It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.
 
-Roughly, the idea is that a \emph{box} is a container for an proposition $\prop$.
+Roughly, the idea is that a \emph{box} is a container for a proposition $\prop$.
 A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.
 Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).
 The proposition governing the box keeps track of the state of all the slices that make up the box.
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 557c8c64df2ae90436856d41436dfe1c3722403b..5404f658249d5868012479ba91c725e21bfd0428 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -23,7 +23,7 @@ We assume to have the following four cameras available:
 \end{align*}
 The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
 
-We assume that at the beginning of the verification, instances named $\gname_{\textdom{State}}$, $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
+We assume that at the beginning of the verification, instances named $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
 
 \paragraph{World Satisfaction.}
 We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 50f03e157d61c5917833141a49e896d075175ebf..9c1d7af95e05a9d120ed2ca5facdee8b2c6dbb2a 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -308,7 +308,7 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
    The reason for this is that if given an evar, these typeclasses
    would typically try to instantiate this evar with some arbitrary
-   logical constructs such as emp or True. Therefore, we use an Hint
+   logical constructs such as emp or True. Therefore, we use a Hint
    Mode to disable all the instances that would have this behavior. *)
 Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.