diff --git a/doc/coq.rst b/doc/coq.rst index 0cd74e15d53f..eefd31aaa3fb 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -59,6 +59,7 @@ stanza: (modules ) (plugins ) (flags ) + (coqdoc_flags ) (stdlib ) (mode ) (theories )) @@ -106,6 +107,11 @@ The semantics of the fields are: is taken from the value set in the ``(coq (flags ))`` field in ``env`` profile. See :ref:`dune-env` for more information. +- ```` are extra user-configurable flags passed to ``coqdoc``. The + default value for ``:standard`` is ``--toc``. The ``--html`` or ``--latex`` + flags are passed separately depending on which mode is targed. See the section + on :ref:`documentation using coqdoc` for more information. + - ```` can either be ``yes`` or ``no``, currently defaulting to ``yes``. When set to ``no``, Coq's standard library won't be visible from this theory, which means the ``Coq`` prefix won't be bound, and @@ -150,6 +156,7 @@ them in the correct order, even if they are in separate theories. Under the hood, Dune asks coqdep how to resolve these dependencies, which is why it is called once per theory. +.. coqdoc:: Coq Documentation ~~~~~~~~~~~~~~~~~ @@ -161,7 +168,13 @@ A.tex``, respectively (if the :ref:`dune file` for the theory is the current directory). There are also two aliases ``@doc`` and ``@doc-latex`` that will respectively -build the HTML or LaTeX documentation when called. +build the HTML or LaTeX documentation when called. These will determine whether +or not Dune passes a ``--html`` or ``--latex`` flag to ``coqdoc``. + +Further flags can also be configured using the ```` field in the +``coq.theory`` stanza. These will be passed to ``coqdoc`` and the default value +is ``:standard`` which is ``--toc``. Extra flags can therefore be passed by +writing ``(coqdoc_flags :standard --body-only)`` for example. .. _include-subdirs-coq: