diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v index 28147e995a4a4c42f524068ee5947caea5eb1571..cf118ab660de11b0d9ac2b96398f1ec6d505c019 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 32acfe20dbe2d4ed2546a83440a165971c35bb95..4e422856398f825dcab94426321f0e0fa8c07998 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 27ad69efcd1ab038adafa887c153207abdf69b27..9cfc2beb494b1ebeb943f1a4d292952363fff2e0 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.