Commit 0e1bdaf4 authored by Ralf Jung's avatar Ralf Jung
Browse files

better error for iModIntro on mask-changing update

parent 15946faa
......@@ -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).
......
......@@ -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
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment