From d6412b3a98c81de41ec15e31ba1923bd24157bb6 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Thu, 29 Jul 2021 11:35:15 -0700
Subject: [PATCH] fix: pp.analyze was still printing inaccessibles

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 292af5fc4f..ecc59911b7 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -360,7 +360,7 @@ where
               match instResult with
               | LOption.some inst =>
                 if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip
-                else annotateBool `pp.analysis.namedArg
+                else discard <| annotateNamedArg (← mvarName mvars[i]) appPos
               | _                 => discard <| annotateNamedArg (← mvarName mvars[i]) appPos
           | BinderInfo.auxDecl        => pure ()
           | BinderInfo.strictImplicit => unreachable!