From 65b45fe6e86cc8b642069e33c3b7073f48b592a9 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 26 Nov 2015 15:56:47 +0100 Subject: Partially fixing #4408: coqdep --help is up to date. --- tools/coqdep.ml | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index e0e017e88a..e51572fc35 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -426,12 +426,25 @@ let coq_dependencies_dump chan dumpboxes = end let usage () = - eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-Q dir coqdir] [-R dir coqdir] +\n"; - eprintf " extra options:\n"; - eprintf " -sort : output the file names ordered by dependencies\n"; - eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -exclude-dir f : skip subdirectories named 'f' during -R search\n"; + eprintf " usage: coqdep [options] +\n"; + eprintf " options:\n"; + eprintf " -c : \n"; + eprintf " -D : \n"; + eprintf " -w : \n"; + eprintf " -boot : \n"; + eprintf " -sort : output the given file name ordered by dependencies\n"; + eprintf " -noglob | -no-glob : \n"; + eprintf " -I dir -as logname : adds (non recursively) dir to coq load path under logical name logname\n"; + eprintf " -I dir : adds (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 (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; + eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; + eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R search\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -suffix s : \n"; + eprintf " -slash : deprecated, no effect\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) -- cgit v1.2.3 From d6d81d63591e37fd74c841165afd9e3baf6e0d8d Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 13 Nov 2015 15:56:47 +0100 Subject: Fix #4408. Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others. --- tools/coqdep.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index e51572fc35..011293a901 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -428,10 +428,13 @@ end let usage () = eprintf " usage: coqdep [options] +\n"; eprintf " options:\n"; - eprintf " -c : \n"; - eprintf " -D : \n"; - eprintf " -w : \n"; - eprintf " -boot : \n"; + eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; + (* Does not work anymore *) + (* eprintf " -w : Print informations on missing or wrong \"Declare + ML Module\" commands in coq files.\n"; *) + (* Does not work anymore: *) + (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) + eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; eprintf " -I dir -as logname : adds (non recursively) dir to coq load path under logical name logname\n"; @@ -441,7 +444,7 @@ let usage () = eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; - eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R search\n"; + eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; -- cgit v1.2.3 From 088977e086a5fd72f5f724192e5cb5ba1a0d9bb6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:30:00 +0100 Subject: Minor edits in output of coqdep --help. --- tools/coqdep.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 011293a901..aaea1ee703 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -437,8 +437,8 @@ let usage () = eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; - eprintf " -I dir -as logname : adds (non recursively) dir to coq load path under logical name logname\n"; - eprintf " -I dir : adds (non recursively) dir to ocaml path\n"; + 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 (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- tools/compat5.ml | 2 +- tools/compat5.mlp | 2 +- tools/compat5b.ml | 2 +- tools/compat5b.mlp | 2 +- tools/coq_makefile.ml | 2 +- tools/coq_tex.ml | 2 +- tools/coqc.ml | 2 +- tools/coqdep.ml | 2 +- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 2 +- tools/coqdep_common.mli | 2 +- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 2 +- tools/coqdoc/index.ml | 2 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 2 +- tools/coqdoc/output.mli | 2 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqmktop.ml | 2 +- tools/coqwc.mll | 2 +- tools/coqworkmgr.ml | 2 +- tools/fake_ide.ml | 2 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- 31 files changed, 31 insertions(+), 31 deletions(-) (limited to 'tools') diff --git a/tools/compat5.ml b/tools/compat5.ml index 041ced0044..33c1cd602b 100644 --- a/tools/compat5.ml +++ b/tools/compat5.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*