diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 7567cff8da..87a7d4f011 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1117,9 +1117,12 @@ where
     withTypeAscription (cond := ← getPPOption getPPCoercionsTypes) do
       guard <| !insertExplicit
       if info.type == .coeFun && nargs > 0 then
-        -- In the CoeFun case, annotate with the coercee itself.
+        -- In the `.coeFun` case, delaborate the coercee itself.
         -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
-        withNaryArg info.coercee <| withAnnotateTermInfo delab
+        -- In the `pp.tagAppFns` case, if the coercee is a constant application,
+        -- then `delab` will tag the result with the constant, ensuring docgen linkifies it.
+        let tagAppFns ← getPPOption getPPTagAppFns
+        withNaryArg info.coercee <| withOptionAtCurrPos `pp.tagAppFns tagAppFns delab
       else
         withAnnotateTermInfo do
           match info.type with