From b596073140307ec8eeb5b45d4908959ca97d917d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 21 May 2021 09:36:17 +0200
Subject: [PATCH] Fix typo

---
 iris/proofmode/classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index a57e644d8..a647713aa 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -247,7 +247,7 @@ Global Hint Mode IsExcept0 + ! : typeclass_instances.
 The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].
 
 The class is used to transform a hypothesis [P] into a hypothesis [P'], given
-a goal [Q], which is simultaniously transformed into [Q']. The Booleans [p]
+a goal [Q], which is simultaneously transformed into [Q']. The Booleans [p]
 and [p'] indicate whether the original, respectively, updated hypothesis reside
 in the persistent context (iff [true]). The proposition [φ] can be used to
 express a side-condition that [iMod] will generate (if not [True]).
-- 
GitLab