This PR fixes an "Unknown constant" error when `set_option diagnostics
true` is enabled in module mode under a `public section`. Diagnostic
output may reference private declarations such as `_match_*` and
`_sparseCasesOn_*` that are recorded in unfold counters; constructing
the message previously failed because the environment was in exporting
mode and could not resolve those names. The diagnostic-printing paths in
`Lean.Meta.Diagnostics.reportDiag` and
`Lean.Meta.Tactic.Simp.Diagnostics.reportDiag` now run under
`withoutExporting`.
Closes https://github.com/leanprover/lean4/issues/13581.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
