From 07d25e678cf436be61097c73a7341362e3ffeb57 Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 29 Oct 2020 09:16:30 +0100
Subject: [PATCH] Fix typos

---
 README.md                         | 4 ++--
 docs/heap_lang.md                 | 2 +-
 docs/proof_mode.md                | 2 +-
 tex/constructions.tex             | 2 +-
 tex/extended-logic.tex            | 8 ++++----
 tex/program-logic.tex             | 4 ++--
 theories/proofmode/ltac_tactics.v | 2 +-
 7 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/README.md b/README.md
index 1f76da797..c8107d947 100644
--- a/README.md
+++ b/README.md
@@ -51,7 +51,7 @@ To obtain a development version, also add the Iris opam repository:
     opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
 Either way, you can now do `opam install coq-iris`.  To fetch updates later, run
-`opam update && opam upgrade`.  However, notice that we do not guarnatee
+`opam update && opam upgrade`.  However, notice that we do not guarantee
 backwards-compatibility, so upgrading Iris may break your Iris-using
 developments.
 
@@ -87,7 +87,7 @@ followed by `make build-dep`.
   the primitive connectives.  It also contains derived constructions that are
   entirely independent of the choice of resources.
   * The subfolder [lib](theories/base_logic/lib) contains some generally useful
-    derived constructions.  Most importantly, it defines composeable
+    derived constructions.  Most importantly, it defines composable
     dynamic resources and ownership of them; the other constructions depend
     on this setup.
 * The folder [program_logic](theories/program_logic) specializes the base logic
diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index 682410d3a..a80047d3a 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -114,7 +114,7 @@ all of the redexes reduced.)
 ## Notation and lemmas for derived notions involving a thunk
 
 Sometimes, it is useful to define a derived notion in HeapLang that involves
-thunks.  For example, the parallel composition `e1 ||| e2` is defineable in
+thunks.  For example, the parallel composition `e1 ||| e2` is definable in
 HeapLang, but that requires thunking `e1` and `e2` before passing them to
 `par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).)  However,
 this is somewhat subtle because of the distinction between expression lambdas
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 6e9cdbaac..45fcf8aa7 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -120,7 +120,7 @@ Separation logic-specific tactics
   This tactic solves the goal if everything in the conclusion has been framed.
 - `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
   `H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
-- `iAccu` : solves a goal that is an evar by instantiating it with a all
+- `iAccu` : solves a goal that is an evar by instantiating it with all
   hypotheses from the spatial context joined together with a separating
   conjunction (or `emp` in case the spatial context is empty).
 
diff --git a/tex/constructions.tex b/tex/constructions.tex
index f1e0a10c2..acaa76a10 100644
--- a/tex/constructions.tex
+++ b/tex/constructions.tex
@@ -7,7 +7,7 @@ This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$
 
 \subsection{Next (Type-Level Later)}
 
-Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
+Given an OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
 \begin{align*}
   \latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
   \latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
diff --git a/tex/extended-logic.tex b/tex/extended-logic.tex
index 3d1ae27b4..f52d3a4dc 100644
--- a/tex/extended-logic.tex
+++ b/tex/extended-logic.tex
@@ -78,7 +78,7 @@ As already mentioned, the persistence modality is an always-style modality:
   {}{\always\always\prop \provesIff \always\prop}
 \end{mathpar}
 Some further interesting derived rules include:
-\begin{mathparpagebreakable}  
+\begin{mathparpagebreakable}
   \infer{}
   {\always(\prop\land\propB) \provesIff \always\prop \land \always\propB}
 
@@ -300,8 +300,8 @@ The following rules identify the class of timeless propositions:
 \end{mathparpagebreakable}
 
 
-\subsection{Dynamic Composeable Higher-Order Resources}
-\label{sec:composeable-resources}
+\subsection{Dynamic Composable Higher-Order Resources}
+\label{sec:composable-resources}
 
 The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
 It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of propositions themselves.
@@ -348,7 +348,7 @@ Effectively, we just defined a way to instantiate the base logic with $\Res$ as
 We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
 
 \paragraph{Proof composability.}
-To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
+To make our proofs composable, we \emph{generalize} our proofs over the family of functors.
 This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product ``pointwise''.
 So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
 Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 2983ceb39..557c8c64d 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -4,7 +4,7 @@
 
 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic.
 So in the following, we assume that some language $\Lang$ was fixed.
-Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composeable-resources}.
+Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composable-resources}.
 
 
 \subsection{World Satisfaction, Invariants, Fancy Updates}
@@ -398,7 +398,7 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
 
 The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
 They, too, are lists of $\nat$, the same type as namespaces.
-In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of ``plain'' invariant names.
+In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structured invariant names to $\InvName$, the type of ``plain'' invariant names.
 Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.
 Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index ce7677545..6cd5e2e4c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -81,7 +81,7 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
   lazymatch goal with
   | |- @envs_entails ?PROP' _ _ =>
     (* This cannot be shared with the other [iStartProof], because
-    type_term has a non-negligeable performance impact. *)
+    type_term has a non-negligible performance impact. *)
     let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
 
   (* We eta-expand [as_emp_valid_2], in order to make sure that
-- 
GitLab