From 1cc82281bfa37c1a33b5ea82d1ecf1ea1f783888 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Sun, 12 Apr 2020 21:36:38 -0400
Subject: [PATCH] typo

---
 MessagesAndRefinement.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v
index 4f22534..0a2dc74 100644
--- a/MessagesAndRefinement.v
+++ b/MessagesAndRefinement.v
@@ -205,7 +205,7 @@ Definition simulates (R : proc -> proc -> Prop) (pr1 pr2 : proc) :=
                                    -> exists pr2', lstepSilent^* pr2 pr2'
                                                    /\ R pr1' pr2')
 
-  (* Now consider the same scenario where the lefthand process make a nonsilent
+  (* Now consider the same scenario where the lefthand process takes a nonsilent
    * step.  We require that the righthand process can "catch up" in a way that
    * generates the same label that the lefthand process generated. *)
   /\ (forall pr1 pr2, R pr1 pr2