From 1ee1d9f9f50fae11705756873e6be02e1b3744bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 Jul 2019 14:21:27 +0200
Subject: [PATCH] Make `iPure` non-local so it can be used for defining custom
`iDestruct`-like tactics.
---
theories/proofmode/ltac_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index cc6bac66f..81e03f9a5 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -296,7 +296,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
fail "iIntuitionistic:" P "not affine and the goal not absorbing"
|pm_reduce].
-Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
+Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with H _ _ _; (* (i:=H1) *)
[pm_reflexivity ||
let H := pretty_ident H in
--
GitLab