From a3775658c2dda7295274f571c6f2b6882d219af0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Feb 2018 23:17:30 +0100
Subject: [PATCH] Less hacky fix than d1b836c8.
---
theories/proofmode/tactics.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6d832da44..6ddb46dae 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -964,8 +964,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Modality introduction *)
Tactic Notation "iModIntro" open_constr(M) :=
iStartProof;
- let bi := lazymatch goal with |- @envs_entails ?bi _ _ => bi end in
- eapply (tac_modal_intro (PROP2 := bi)) with M _ _ _ _;
+ notypeclasses refine (tac_modal_intro M _ _ _ _ _ _ _ _ _ _ _ _);
[apply _ ||
fail "iModIntro: the goal is not a modality"
|apply _ ||
--
GitLab