diff --git a/CHANGELOG.md b/CHANGELOG.md
index f93680cbf4ee084c54cc456c2e05423d59872f8a..0317a71b374ccfd093ffc29437fb6f530b23fc91 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,7 +51,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add support for destructing existentials with the intro pattern `[%x ...]`.
   (by Tej Chajed)
 * `iMod`/`iModIntro` show proper error messages when they fail due to mask
-  mismatches.
+  mismatches. To support this, the proofmode typeclass `FromModal` now takes an
+  additional pure precondition.
 
 **Changes in `bi`:**
 
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 339e7e2f5093ba000f88992b07626ff8b7389985..0767cdf874ee7121b1a258c44606e1fd68671ba7 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -96,7 +96,7 @@ Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Global Arguments into_persistent {_} _ _%I _%I {_}.
 Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to
+(** The [FromModal φ M sel P Q] class is used by the [iModIntro] tactic to
 transform a goal [P] into a modality [M] and proposition [Q], under additional
 pure assumptions [φ].
 
@@ -109,7 +109,7 @@ or embedding, respectively. In case there is no need to specify the modality to
 introduce, [sel] should be an evar.
 
 For modalities [N] that do not need to augment the proof mode environment, one
-can define an instance [FromModal modality_id (N P) P]. Defining such an
+can define an instance [FromModal True modality_id (N P) P]. Defining such an
 instance only imposes the proof obligation [P ⊢ N P]. Examples of such
 modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 [bi_absorbingly]. *)
diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index 7b215c7e3665086b2d5e982755290fa1190e0a88..37094e2a72d5ce6cd9d52c8a2209bf58e2b75ae0 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -178,8 +178,8 @@ Section modality1.
 End modality1.
 
 (** The identity modality [modality_id] can be used in combination with
-[FromModal modality_id] to support introduction for modalities that enjoy
-[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
+[FromModal True modality_id] to support introduction for modalities that enjoy
+[P ⊢ M P]. This is done by defining an instance [FromModal True modality_id (M P) P],
 which will instruct [iModIntro] to introduce the modality without modifying the
 proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
 [monPred_subjectively] and [bi_absorbingly]. *)