From 0e1bdaf4b28d92d62b68340c7fc0b5a0c1688b93 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 May 2021 16:38:32 +0200
Subject: [PATCH] better error for iModIntro on mask-changing update
---
iris/proofmode/class_instances_updates.v | 6 ++++++
tests/proofmode.ref | 10 ++++++++++
tests/proofmode.v | 9 +++++++++
3 files changed, 25 insertions(+)
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 28147e995..cf118ab66 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -129,6 +129,12 @@ Proof. by rewrite /FromModal /= -bupd_intro. Qed.
Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
+Global Instance from_modal_fupd_wrong_mask E1 E2 P `{!BiFUpd PROP} :
+ FromModal
+ (pm_error "Only non-mask-changing update modalities can be introduced directly.
+Use [iApply fupd_mask_intro] to introduce mask-changing update modalities")
+ modality_id (|={E1,E2}=> P) (|={E1,E2}=> P) P | 100.
+Proof. by intros []. Qed.
Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 32acfe20d..4e4228563 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -717,6 +717,16 @@ The command has indeed failed with message:
Tactic failure:
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
+"iModIntro_mask_mismatch"
+ : string
+The command has indeed failed with message:
+Tactic failure:
+"Only non-mask-changing update modalities can be introduced directly.
+Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
+The command has indeed failed with message:
+Tactic failure:
+"Only non-mask-changing update modalities can be introduced directly.
+Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
"test_pure_name"
: string
1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 27ad69efc..9cfc2beb4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1401,6 +1401,15 @@ Proof.
Fail iIntros ">HP".
iIntros "HP". Fail iMod "HP".
Abort.
+
+Check "iModIntro_mask_mismatch".
+Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
+ ⊢ |={E1,E2}=> P.
+Proof.
+ Fail iModIntro.
+ Fail iIntros "!>".
+Abort.
+
End error_tests.
Section pure_name_tests.
--
GitLab