aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-01 13:51:27 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-06 22:31:22 +0100
commitd3414abd4dc912debf1a8339eedbe1b9d4dbc319 (patch)
tree909c0a98f84f75a6a0d876fd04078b6774437776
parented98716036e9d47efb2ba66cf0336fc45e03f793 (diff)
Add CHANGES and man entry for coqdep learning _CoqProject.
-rw-r--r--CHANGES6
-rw-r--r--man/coqdep.13
2 files changed, 9 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2040c1b57..b0843a621 100644
--- a/CHANGES
+++ b/CHANGES
@@ -93,6 +93,12 @@ CoqIDE
- Find and Replace All report the number of occurrences found; Find indicates
when it wraps.
+coqdep
+
+- Learned to read -I, -Q, -R and filenames from _CoqProject files.
+ This is used by coq_makefile when generating dependencies for .v
+ files (but not other files).
+
Documentation
- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
diff --git a/man/coqdep.1 b/man/coqdep.1
index ed727db7c..c417402c2 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -80,6 +80,9 @@ Prints the dependencies of Caml modules.
\" 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.
.TP
.BI \-I/\-Q/\-R \ options
Have the same effects on load path and modules names as for other