From c8079d986234259be2170efba09d406ec1e934fe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 13:54:07 +0100
Subject: [PATCH] Version of `iModIntro` where one can specify the modality.
---
theories/proofmode/tactics.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 3a0401699..822786b44 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -962,9 +962,9 @@ Local Tactic Notation "iExistDestruct" constr(H)
|revert y; intros x].
(** * Modality introduction *)
-Tactic Notation "iModIntro":=
+Tactic Notation "iModIntro" open_constr(M) :=
iStartProof;
- eapply tac_modal_intro;
+ eapply tac_modal_intro with M _ _ _ _;
[apply _ ||
fail "iModIntro: the goal is not a modality"
|apply _ ||
@@ -982,6 +982,7 @@ Tactic Notation "iModIntro":=
|env_cbv; apply _ ||
fail "iModIntro: cannot filter spatial context when goal is not absorbing"
|].
+Tactic Notation "iModIntro" := iModIntro _.
Tactic Notation "iAlways" := iModIntro.
(** * Later *)
--
GitLab