diff options
| author | Emilio Jesus Gallego Arias | 2020-02-12 23:12:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 22:11:05 +0100 |
| commit | 8d73861eeae56321a106f28d07b47d5d6699939d (patch) | |
| tree | 31e8ee4a328798a9269141dab30c77e70b78bdfd /man | |
| parent | 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f (diff) | |
[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.
Diffstat (limited to 'man')
| -rw-r--r-- | man/coqdep.1 | 30 |
1 files changed, 1 insertions, 29 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1 index 4223482c99..0770ce88c8 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -12,9 +12,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .BI \-coqlib \ directory ] [ -.BI \-c -] -[ .BI \-i ] [ @@ -52,10 +49,6 @@ directives and the dot notation .SH OPTIONS .TP -.BI \-c -Prints the dependencies of Caml modules. -(On Caml modules, the behaviour is exactly the same as ocamldep). -.TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP @@ -152,29 +145,8 @@ example% coqdep \-I . *.v .fi .RE .br -.ne 7 -.LP -To get only the Caml dependencies: -.IP -.B -example% coqdep \-c \-I . *.ml -.RS -.sp .5 -.nf -.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo -.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx -.B C.cmo: C.ml -.B C.cmx: C.ml -.B B.cmo: B.ml -.B B.cmx: B.ml -.B A.cmo: A.ml -.B A.cmx: A.ml -.fi -.RE -.br -.ne 7 .SH BUGS Please report any bug to -.B coq\-bugs@pauillac.inria.fr +.B https://github.com/coq/coq/issues |