diff --git a/doc/dune-files.rst b/doc/dune-files.rst index 58d4af32fa47..f07148995b55 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1657,6 +1657,9 @@ process. This is done using the ``coq.extract`` stanza: - ```` are ``flags``, ``theories``, and ``libraries``. All of these fields have the same meaning as in the ``coq.theory`` stanza. +The extracted sources can then in ``executable`` or ``library`` stanzas as any +other sources. + .. _dune-workspace: mdx (since 2.4)