Commit d1b836c8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make sure iNext works even if the entailment is not directly an sbi entailment.

parent ad908d6e
Pipeline #7119 passed with stage
in 10 minutes and 48 seconds
......@@ -964,7 +964,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Modality introduction *)
Tactic Notation "iModIntro" open_constr(M) :=
iStartProof;
eapply tac_modal_intro with M _ _ _ _;
let bi := lazymatch goal with |- @envs_entails ?bi _ _ => bi end in
eapply (tac_modal_intro (PROP2 := bi)) with M _ _ _ _;
[apply _ ||
fail "iModIntro: the goal is not a modality"
|apply _ ||
......
......@@ -114,4 +114,8 @@ Section tests.
iIntros "[$ #HP]". iFrame "HP".
Qed.
Lemma test_iNext_Bi P :
@bi_entails monPredI ( P) ( P).
Proof. iIntros "H". by iNext. Qed.
End tests.
Markdown is supported
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