aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--tools/coqdep.ml2
2 files changed, 1 insertions, 3 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 9097195721..0086516785 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -467,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok)
.PHONY: vok
validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+ $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
.PHONY: validate
only: $(TGTS)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 20ffdfe81d..2177da0c75 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -35,9 +35,7 @@ let usage () =
eprintf " -sort : output the given file name ordered by dependencies\n";
eprintf " -noglob | -no-glob : \n";
eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.";
- eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";
eprintf " -I dir : add (non recursively) dir to ocaml path\n";
- eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *)
eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n";
eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n";
eprintf " -vos : also output dependencies about .vos files\n";