From 8d73861eeae56321a106f28d07b47d5d6699939d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 12 Feb 2020 23:12:26 +0100
Subject: [coqdep] Remove support for `-c` ocamldep replacement.

There is not need for coqdep to ship an `ocamldep` replacement, in
particular:

- not used in the main build since a long time
- not tested
- not kept up to date with upstream

This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.

`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.

We also remove the residual `-slash` option.
---
 doc/sphinx/practical-tools/utilities.rst | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3