From 5ac41ebcec7fad55efd8ecbfb1620ff51af201ca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Jun 2021 11:26:06 +0200
Subject: [PATCH] changelog and comment fixes for FromModal changes

---
 CHANGELOG.md                | 3 ++-
 iris/proofmode/classes.v    | 4 ++--
 iris/proofmode/modalities.v | 4 ++--
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f93680cbf..0317a71b3 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 339e7e2f5..0767cdf87 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 7b215c7e3..37094e2a7 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]. *)
-- 
GitLab