From e4865f5aadef4f8b321603766a2dff12433693c0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jul 2020 14:58:19 -0700
Subject: [PATCH] fix: `resolveGlobalName` for atomic references to private
 names

---
 src/Lean/Elab/ResolveName.lean | 2 ++
 tests/lean/run/prv.lean        | 7 +++++++
 2 files changed, 9 insertions(+)
 create mode 100644 tests/lean/run/prv.lean

diff --git a/src/Lean/Elab/ResolveName.lean b/src/Lean/Elab/ResolveName.lean
index 52e09af507..b7d03feb70 100644
--- a/src/Lean/Elab/ResolveName.lean
+++ b/src/Lean/Elab/ResolveName.lean
@@ -88,6 +88,8 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li
   | some newId => [(newId, projs)]
   | none =>
   let resolvedIds := if env.contains id then [id] else [];
+  let idPrv := mkPrivateName env id;
+  let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds;
   let resolvedIds := resolveOpenDecls env id openDecls resolvedIds;
   let resolvedIds := getAliases env id ++ resolvedIds;
   match resolvedIds with
diff --git a/tests/lean/run/prv.lean b/tests/lean/run/prv.lean
new file mode 100644
index 0000000000..3e0a37c05b
--- /dev/null
+++ b/tests/lean/run/prv.lean
@@ -0,0 +1,7 @@
+new_frontend
+
+private def x := 10
+
+#check _root_.x
+#check x
+#eval x + 1