From d1b836c836776d4dd48ab75894ee3c30b5b965b6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 28 Feb 2018 22:39:14 +0100
Subject: [PATCH] Make sure iNext works even if the entailment is not directly
an sbi entailment.
---
theories/proofmode/tactics.v | 3 ++-
theories/tests/proofmode_monpred.v | 4 ++++
2 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index c50c6dbd8..6d832da44 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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 _ ||
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index af40b762f..efdff6378 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -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.
--
GitLab