From ae69f50b7245dcc223c93b10992daeff1b661bb6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Thu, 29 Oct 2020 14:49:07 +0900
Subject: [PATCH] fix typos

---
 README.md                  | 2 +-
 theories/typing/own.v      | 2 +-
 theories/typing/type_sum.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 3f3d91cb..6d689102 100644
--- a/README.md
+++ b/README.md
@@ -91,7 +91,7 @@ borrows" in the Coq development.
 | F-endlft              | programs.v      | type_endlft           |
 | F-call                | function.v      | type_call'            |
 
-Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
+Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
 
 ### Lifetime Logic Rules
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 2deec3a4..de9046c5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -16,7 +16,7 @@ Section own.
     end%I.
   Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
   Arguments freeable_sz : simpl never.
-  Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
+  Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
   Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index d61c770b..a8c4d60b 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Section case.
   Context `{!typeG Σ}.
 
-  (* FIXME : have a iris version of Forall2. *)
+  (* FIXME : have an Iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
       (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
-- 
GitLab