aboutsummaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-05 12:53:37 +0100
committerGaƫtan Gilbert2020-02-07 13:24:53 +0100
commitfe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d (patch)
treefe8cb673c25933481965df0b62301e0e0b71d493 /man
parentadf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff)
[coqdep] Remove dumpgraph and broken options
We remove the `dumpgraph` option which was causing quite a bit of duplication, we also clean up options marked as broken `-w/-D`
Diffstat (limited to 'man')
-rw-r--r--man/coqdep.131
1 files changed, 1 insertions, 30 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1
index 02c9d4390c..4223482c99 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -6,9 +6,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
.SH SYNOPSIS
.B coqdep
[
-.BI \-w
-]
-[
.BI \-I \ directory
]
[
@@ -21,9 +18,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
.BI \-i
]
[
-.BI \-D
-]
-[
.BI \-slash
]
.I filename ...
@@ -61,25 +55,6 @@ directives and the dot notation
.BI \-c
Prints the dependencies of Caml modules.
(On Caml modules, the behaviour is exactly the same as ocamldep).
-\" THESE OPTIONS ARE BROKEN CURRENTLY
-\" .TP
-\" .BI \-w
-\" Prints a warning if a Coq command
-\" .IR Declare \&
-\" .IR ML \&
-\" .IR Module \&
-\" is incorrect. (For instance, you wrote `Declare ML Module "A".',
-\" but the module A contains #open "B"). The correct command is printed
-\" (see option \-D). The warning is printed on standard error.
-\" .TP
-\" .BI \-D
-\" This commands looks for every command
-\" .IR Declare \&
-\" .IR ML \&
-\" .IR Module \&
-\" of each Coq file given as argument and complete (if needed)
-\" the list of Caml modules. The new command is printed on
-\" the standard output. No dependency is computed with this option.
.TP
.BI \-f \ file
Read filenames and options -I, -R and -Q from a _CoqProject FILE.
@@ -93,10 +68,6 @@ Indicates where is the Coq library. The default value has been
determined at installation time, and therefore this option should not
be used under normal circumstances.
.TP
-.BI \-dumpgraph[box] \ file
-Dumps a dot dependency graph in file
-.IR file \&.
-.TP
.BI \-exclude-dir \ dir
Skips subdirectory
.IR dir \ during
@@ -169,7 +140,7 @@ example% coqdep \-I . *.v
With a warning:
.IP
.B
-example% coqdep \-w \-I . *.v
+example% coqdep \-I . *.v
.RS
.sp .5
.nf