Commit 1ee1d9f9 authored by Robbert Krebbers's avatar Robbert Krebbers

Make `iPure` non-local so it can be used for defining custom `iDestruct`-like tactics.

parent 24ee24e2
...@@ -296,7 +296,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) := ...@@ -296,7 +296,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
fail "iIntuitionistic:" P "not affine and the goal not absorbing" fail "iIntuitionistic:" P "not affine and the goal not absorbing"
|pm_reduce]. |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) *) eapply tac_pure with H _ _ _; (* (i:=H1) *)
[pm_reflexivity || [pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
......
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