diff options
| author | Gaëtan Gilbert | 2020-02-17 13:25:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-17 13:25:21 +0100 |
| commit | cd7323ce0f7648f6db732292c0ded05c480be71f (patch) | |
| tree | dc9056daf8854dec4342b361010035153c56949f /doc | |
| parent | d122f7d5ffd5d3b26153a0ad7b74a669b8dd1c9d (diff) | |
| parent | 8d73861eeae56321a106f28d07b47d5d6699939d (diff) | |
Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..3d1fc6d4b9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -545,7 +545,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the |