diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index cc6bac66fdb0dbde4197adab07e000c83f2a3617..81e03f9a56d3ff0eaf33933bc8800bd5ab21b900 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