Private names are pretty-printed without considering open namespaces

[Rob23oba]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Private names are always pretty-printed in full length. This is inconsistent with regular names, which take open namespaces into account.

Context

Verification of private functions via import all.

Steps to Reproduce

module
import all Init.Prelude

open Lean Name

/-- info: Lean.eraseMacroScopesAux✝ : Name → Name -/
#guard_msgs in #check (eraseMacroScopesAux)

/-- info: eraseMacroScopes : Name → Name -/
#guard_msgs in #check (eraseMacroScopes)

Expected behavior:
Neither of the name has the prefix Lean pretty-printed.

Actual behavior:
The private name includes the prefix Lean after pretty-printing.

Versions

Lean 4.25.0-nightly-2025-10-13

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.