From 5a8f9ace72ac552cbaf4a00a44b0bfabe525d794 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Oct 2022 07:39:06 -0700
Subject: [PATCH] fix: `open .. hinding ..` should activate scoped attributes

---
 src/Lean/Elab/Open.lean                |  1 +
 tests/lean/run/scopedHindingIssue.lean | 13 +++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/run/scopedHindingIssue.lean

diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean
index 196dc4c786..d47bdb33e6 100644
--- a/src/Lean/Elab/Open.lean
+++ b/src/Lean/Elab/Open.lean
@@ -76,6 +76,7 @@ def elabOpenDecl [MonadResolveName m] (stx : TSyntax ``Parser.Command.openDecl)
         addOpenDecl (OpenDecl.explicit idStx.getId declName)
     | `(Parser.Command.openDecl| $ns hiding $ids*) =>
       let ns ← resolveUniqueNamespace ns
+      activateScoped ns
       for id in ids do
         let _ ← resolveId ns id
       let ids := ids.map (·.getId) |>.toList
diff --git a/tests/lean/run/scopedHindingIssue.lean b/tests/lean/run/scopedHindingIssue.lean
new file mode 100644
index 0000000000..ac92c1705d
--- /dev/null
+++ b/tests/lean/run/scopedHindingIssue.lean
@@ -0,0 +1,13 @@
+namespace Foo
+
+def x := 10
+
+scoped macro "~0~" : term => `(0)
+
+#check ~0~
+
+end Foo
+
+open Foo hiding x -- must open scoped notation and attributes too
+
+#check ~0~