diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index ff248cc620..e9ac7a1ee2 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -51,8 +51,8 @@ def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [M if getLinterValue linter.deprecated (← getOptions) then let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure () logWarning <| .tagged ``deprecatedAttr <| - s!"`{declName}` has been deprecated" ++ match attr.text? with + m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with | some text => s!": {text}" | none => match attr.newName? with - | some newName => s!": use `{newName}` instead" + | some newName => m!": use `{.ofConstName newName true}` instead" | none => ""