doc(coq): Add documentation for composition with installed theories

Signed-off-by: Ali Caglayan <alizter@gmail.com>

doc/coq.rst

@@ -28,12 +28,14 @@ collection of Coq theories and plugins.
 The ``.v`` files of a theory need not be present as source files. They may also
 be Dune targets of other rules.
 
+Coq theories may come from the same workspace or from an install location.
+
 To enable Coq support in a Dune project, specify the :ref:`Coq language
 version<coq-lang>` in the :ref:`dune-project` file. For example, adding
 
 .. code:: dune
 
-    (using coq 0.7)
+    (using coq 0.8)
 
 to a :ref:`dune-project` file enables using the ``coq.theory`` stanza and other
 ``coq.*`` stanzas. See the :ref:`Dune Coq language<coq-lang>` section for more
@@ -114,9 +116,10 @@ The semantics of the fields are:
   plugins. Starting with ``(lang coq 0.6)``, ``<ocaml_plugins>`` must contain
   public library names.
 
-- Your Coq theory can depend on other theories by specifying them in the
-  ``<coq_theories>`` field. Dune then passes to Coq the corresponding flags for
-  everything to compile correctly (this corresponds to the ``-Q`` flag for Coq).
+- Your Coq theory can depend on other theories, installed or in your workspace,
+  by specifying them in the ``<coq_theories>`` field. Dune then passes to Coq
+  the corresponding flags for everything to compile correctly (this corresponds
+  to the ``-Q`` flag for Coq).
 
   You may also depend on theories belonging to another :ref:`dune-project` as
   long as they share a common scope under another :ref:`dune-project` file or a
@@ -134,13 +137,15 @@ The semantics of the fields are:
   Interproject composition has been available since :ref:`Coq lang
   0.4<coq-lang>`.
 
-  As of today, Dune cannot depend on installed Coq theories. This restriction
-  will be lifted in the future. Note that composition with the Coq standard
-  library is supported, but in this case the ``Coq`` prefix has been made
-  available in a qualified way, since :ref:`Coq lang 0.2<coq-lang>`.
+  Composition with installed theories has been available since :ref:`Coq lang
+  0.8<coq-lang>`. Instaled theories do not have to be installed using Dune. Dune
+  will scan for theories installed in the ``user-contrib`` directory of the Coq
+  installation or those given in the ``COQPATH`` environment variable.
 
-  You may still use installed libraries in your Coq project, but there is
-  currently no way for Dune to know about it.
+  Composition with the Coq standard library is supported, but in this case the
+  ``Coq`` prefix has been made available in a qualified way, since :ref:`Coq
+  lang 0.2<coq-lang>`. Composition with installed theories is disabled if Coq is
+  found in the workspace, as that always takes precedence.
 
 - From version :ref:`Coq lang 0.7<coq-lang>` onwards, if Coq has been configured
   with ``-native-compiler yes`` or ``ondemand``, Dune will always build the
@@ -244,7 +249,7 @@ file:
 
 .. code:: dune
 
-    (using coq 0.7)
+    (using coq 0.8)
 
 The supported Coq language versions (not the version of Coq) are:
 
@@ -260,6 +265,7 @@ The supported Coq language versions (not the version of Coq) are:
 - ``0.7``: ``(mode )`` is automatically detected from the configuration of Coq
   and ``(mode native)`` is deprecated. The ``dev`` profile also no longer
   disables native compilation.
+- ``0.8``: Support for composition of installed theories.
 
 .. _coq-lang-1.0:
 
@@ -341,7 +347,7 @@ Let us start with a simple project. First, make sure we have a
 .. code:: dune
 
   (lang dune 3.8)
-  (using coq 0.7)
+  (using coq 0.8)
 
 Next we need a :ref:`dune<dune-files>` file with a :ref:`coq-theory` stanza:
 
@@ -494,6 +500,23 @@ All three of the theories we defined before were *private theories*. In order to
 depend on them, we needed to make them *public theories*. See the section on
 :ref:`public-private-theory`.
 
+Composing With Installed Theories
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We can also compose with theories that are installed. If we wanted to have a
+theory that depends on the Coq theory ``mathcomp.ssreflect`` we can add the
+following to our stanza:
+
+.. code:: dune
+
+  (coq.theory
+   (name my_mathcomp_theory)
+   (theories mathcomp.ssreflect))
+
+The ``mathcomp.ssreflect`` theory uses a plugin called ``ssreflect``. In order
+to also use that in this theory, we would need to include it in the
+``(plugins)`` field.
+
 Building Documentation
 ~~~~~~~~~~~~~~~~~~~~~~
 
@@ -551,7 +574,7 @@ otherwise Coq will not be able to find it.
 .. code:: dune
 
   (lang dune 3.8)
-  (using coq 0.7)
+  (using coq 0.8)
 
   (package
    (name my-coq-plugin)