feat: make coeFun delaborator respect pp.tagAppFns (#6729)

This PR makes the pretty printer for `.coeFun`-tagged functions respect
`pp.tagAppFns`. The effect is that in docgen, when an expression pretty
prints as `f x y z` with `f` a coerced function, then if `f` is a
constant it will be linkified.

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