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!