diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 21556d314b5151ea6d94cf2ca6c62aea6f46c0a0..cf2661ddd673845e0130de4d1c57ead057bdb81e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -143,7 +143,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
      let H2 := pretty_ident H2 in
      fail "iRename:" H2 "not fresh"|].
 
-Local Inductive esel_pat :=
+Inductive esel_pat :=
   | ESelPure
   | ESelIdent : bool → ident → esel_pat.