additional details in the doc for -vos

1 files changed, 41 insertions, 10 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index be74b86b30..9da565aa3c 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -257,7 +257,6 @@ and ``coqtop``, unless stated otherwise:
 Compiled interfaces (produced using ``-vos``)
 ----------------------------------------------
 
-
 Compiled interfaces help saving time while developing Coq formalizations,
 by compiling the formal statements exported by a library independently of
 the proofs that it contains.
@@ -269,20 +268,52 @@ the proofs that it contains.
       by producing standard ``.vo`` files. (Technically, when using ``-vos``,
       fewer universe constraints are collected.)
 
-   .. warning::
+**Principle.**
+
+The compilation using ``coqc -vos foo.v`` produces a file called ``foo.vos``,
+which is similar to ``foo.vo`` except that all opaque proofs are skipped in
+the compilation process.
+
+The compilation using ``coqc -vok foo.v`` checks that the file ``foo.v``
+correctly compiles, including all its opaque proofs. If the compilation
+succeeds, then the output is a file called ``foo.vok``, with empty contents.
+This file is only a placeholder indicating that ``foo.v`` has been successfully
+compiled. (This placeholder is useful for build systems such as ``make``.)
+
+When compiling a file ``bar.v`` that depends on ``foo.v`` (for example via
+a ``Require Foo.`` command), if the compilation command is ``coqc -vos bar.v``
+or ``coqc -vok bar.v``, then the file ``foo.vos`` gets loaded (instead of
+``foo.vo``). A special case is if file ``foo.vos`` exists and has empty
+contents, and ``foo.vo`` exists, then ``foo.vo`` is loaded.
+
+Appart from the aforementioned case where ``foo.vo`` can be loaded in place
+of ``foo.vos``, in general the ``.vos`` and ``.vok`` files live totally
+independently from the ``.vo`` files.
+
+**Dependencies generated by ``coq_makefile``.**
+
+The files ``foo.vos`` and ``foo.vok`` both depend on ``foo.v``.
+
+Furthermore, if a file ``foo.v`` requires ``bar.v``, then ``foo.vos``
+and ``foo.vok`` also depend on ``bar.vos``.
 
-      In the current implementation, the use of the command ``Include`` for
-      importing modules compiled using `-vos` might not work properly.
+Note, however, that ``foo.vok`` does not depend on ``bar.vok``.
+Hence, as detailed further, parallel compilation of proofs is possible.
 
+In addition, ``coq_makefile`` generates for a file ``foo.v`` a target
+``foo.required_vos`` which depends on the list of ``.vos`` files that
+``foo.vos`` depends upon (excluding ``foo.vos`` itself). As explained
+next, the purpose of this target is to be able to request the minimal
+working state for editing interactively the file ``foo.v``.
 
-**Typical usage.**
+**Typical compilation of a set of file using a build system.**
 
-Assume a file ``foo.v`` that depends on two files ``bar1.v`` and ``bar2.v``. The
-command ``make foo.requires_vos`` will compile ``bar1.v`` and ``bar2.v`` using
-the option ``-vos`` to skip the proofs, producing ``bar1.vos`` and ``bar2.vos``.
+Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The
+command ``make foo.requires_vos`` will compile ``f1.v`` and ``f2.v`` using
+the option ``-vos`` to skip the proofs, producing ``f1.vos`` and ``f2.vos``.
 At this point, one is ready to work interactively on the file ``foo.v``, even
-though it was never needed to compile the proofs involved in the ``bar*.v``
-files.
+though it was never needed to compile the proofs involved in the files ``f1.v``
+and ``f2.v``.
 
 Assume a set of files ``f1.v ... fn.v`` with linear dependencies. The command
 ``make vos`` enables compiling the statements (i.e. excluding the proofs) in all