Merge PR #21142: Documentation fix

Reviewed-by: jfehrle
Co-authored-by: jfehrle <jfehrle@users.noreply.github.com>

Author: coqbot-app[bot]

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1215,16 +1215,16 @@ Exposing constants to OCaml libraries
    the constant is exposed to the kernel. For instance, the `PrimInt63` module
    features the following declaration:
 
-   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
-   The default is :attr:`global`, even inside sections.
-
    .. rocqdoc::
 
       Register bool as kernel.ind_bool.
 
    This makes the kernel aware of the `bool` type, which is used, for example,
    to define the return type of the :g:`#int63_eq` primitive.
 
+   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
+   The default is :attr:`global`, even inside sections.
+
    .. seealso:: :ref:`primitive-integers`
 
 .. cmd:: Print Registered