changelog and comment fixes for FromModal changes

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`:**
 

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]. *)

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]. *)