fix typos

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
 

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⌝.

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) ::