From 257bd668e43f4280f80905ce9c880f86d790a668 Mon Sep 17 00:00:00 2001
From: Derek Dreyer <dreyer@mpi-sws.org>
Date: Mon, 8 Aug 2016 17:06:59 +0200
Subject: [PATCH] typo fixes

---
 program_logic/counter_examples.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index b539d12f6..f44df277b 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import upred.
 From iris.proofmode Require Import tactics.
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
-name-dependend allocation. *)
+name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context (M : ucmraT).
   Notation iProp := (uPred M).
@@ -139,7 +139,7 @@ Module inv. Section inv.
     apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
   Qed.
 
-  (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
+  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (γ : gname) (P : iProp) : iProp :=
     ∃ i, inv i (start γ ∨ (finished γ ★ □ P)).
   Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
-- 
GitLab