diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index a57e644d8273ca106d8ec72e67e6a12e92c66375..a647713aa2b52ed7fdfa643bc41f80018f261667 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]).