From a16d59ea75be4ffe0a2f8da5f8f4c59f877e26ce Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Mon, 13 Feb 2017 16:14:24 +0100 Subject: [PATCH] When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead. This patch is still not ideal, because some modalities (e.g., later) preserve persistence. --- theories/proofmode/tactics.v | 2 +- theories/tests/proofmode.v | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index 84f4d999d..61762f93c 100644 --- a/theories/proofmode/tactics.v +++ b/theories/proofmode/tactics.v @@ -1247,7 +1247,7 @@ Tactic Notation "iAssertCore" open_constr(Q) |tac H] | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] => let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in - match p with + match eval cbv in (p && negb m) with | false => eapply tac_assert with _ _ _ lr Hs' H Q _; [match m with diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index 459e3198d..8a884b3d7 100644 --- a/theories/tests/proofmode.v +++ b/theories/tests/proofmode.v @@ -124,3 +124,6 @@ Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed. (* Check coercions *) Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed. + +Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P. +Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed. -- GitLab