From d4c1face1e80d0d1028b5d0a05f058937aad53c5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2021 10:55:01 +0100
Subject: [PATCH] fix typo

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

diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index f1255cdc7..a2f494d09 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -30,7 +30,7 @@ Such an action can be one of the following:
   second parameter is the output. Hypotheses that cannot be transformed (i.e.
   for which no instance of `C` can be found) will be cleared.
 - Introduction will clear the context.
-- Introduction will keep the context as-if.
+- Introduction will keep the context as-is.
 
 Formally, these actions correspond to the inductive type [modality_action].
 For each of those actions you have to prove that the transformation is valid.
-- 
GitLab