Description of the problem

.. rocdoc:: always inserts an extra blank line, which doesn't look right. (Note the doc uses :n: heavily, which can create doc hyperlinks for non-terminals but doesn't provide the coloring you get from rocdoc. :n: can also be used in-line rather than becoming a new paragraph.)

   For instance, suppose that we define the following.

   .. rocqdoc::

      Ltac2 Notation foo := fun x => x ().

   Then we have the following expansion at internalization time.

is rendered as

Version of Rocq / Coq where this bug occurs

9.0