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