From 87930f59c3cf3d337b9859601c69acc8d3ee910b Mon Sep 17 00:00:00 2001
From: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Date: Sat, 19 Apr 2025 17:39:16 +0200
Subject: [PATCH] fix: don't reset localInstances in delaboration (#8022)

This PR fixes a bug where pretty printing is done in a context with
cleared local instances. These were cleared since the local context is
updated during a name sanitization step, but preserving local instances
is valid since the modification to the local context only affects user
names.

This showed up when writing the mathlib delaborator for `max` and `min`
(https://github.com/leanprover-community/mathlib4/pull/23558#discussion_r2050787403)
---
 src/Lean/PrettyPrinter.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 6cca1e8a05..e975626230 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -34,7 +34,7 @@ def ppTerm (stx : Term) : CoreM Format := ppCategory `term stx
 
 def ppUsing (e : Expr) (delab : Expr → MetaM Term) : MetaM Format := do
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx #[] do
+  Meta.withLCtx' lctx do
     ppTerm (← delab e)
 
 register_builtin_option pp.exprSizes : Bool := {
@@ -58,7 +58,7 @@ to `Elab.Info` nodes produced by the delaborator at various subexpressions of `e
 def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (delab := Delaborator.delab)
     : MetaM FormatWithInfos := do
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx #[] do
+  Meta.withLCtx' lctx do
     let (stx, infos) ← delabCore e optsPerPos delab
     let fmt ← ppTerm stx >>= maybePrependExprSizes e
     return ⟨fmt, infos⟩