bug: use of wrong docstring for tactic

When creating an automatic list of all tactics in https://leanprover-community.github.io/mathlib-manual/html-multi//Tactics/All-tactics/ we run intro precedence problems when overlapping syntaxes are defined.

I'm not sure this is a bug in Verso , but would very much appreciate any assessment and ideas on how to fix this for us.

Note

It might be that this issue would rather belong to https://github.com/leanprover/reference-manual since I'm observing it in a clone of said repo. I didn't not look deeper into the source.

Reproduction

open the mathlib-manual link to Lean.Parser.Tactic.match
Hovering over match in the docstring of tactic Lean.Parser.Tactic.match shows the docstring from a different tactic match ⋯ with. (link to match ⋯ with.)

The former syntax is in the Lean4 repo (source code) while the latter is in Batteries (source code).

Expected behaviour

I would expect that self-refering syntax like writing match inside it's own docstring would either take higher precedence or prevent a popup alltogether.

Actual behaviour

Writing match always seems to use the docstring of matchWithDot

Context

Zulip report: #mathlib4 > Documentation of all tactics @ 💬

Question

What are the options we'd have to resolve this? Here are a few suggestions:

• Obviously one is to remove the deprecated syntax in Batteries. However, I'm asking because we will have more syntax in downstream projects overwriting Lean4 core tactics.
• Should the deprecated matchWithDot have a @[tactic_alt nomatch] added?
• Should there be some lower priority set on matchWithDot?
• Does matchWithDot somehow need another name so it's not listed as match in the document?

Reproduce the hover behavior from the linked mathlib manual for Lean.Parser.Tactic.match, then compare Lean/Parser/Tactic.lean with Batteries/Tactic/NoMatch.lean, including the referenced syntax declarations. Determine where the overlapping docstring resolution is handled and verify that the intended tactic receives the correct docstring without breaking the other match syntax.