diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-01-04 14:46:52 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-23 10:48:28 +0200 |
| commit | 11ec801fa17434b0a3aad2c88a4422a22f1c4c44 (patch) | |
| tree | f92521f724433aabe365cd4d20f585b1922e5860 /tools | |
| parent | b2b4e85ec6607d7364a0da9c65ae9303b9f73c03 (diff) | |
Put the list of Coq sources subdirectories in one place
and avoid duplication
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0b2c40170..379cc856b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -47,13 +47,7 @@ let section s = (* These are the Coq library directories that are used for * plugin development *) -let lib_dirs = - ["kernel"; "lib"; "library"; "parsing"; - "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; - "vernac"; "stm"; "toplevel"; "grammar"; "config"; - "engine"] - +let lib_dirs = Envars.coq_src_subdirs let usage () = output_string stderr "Usage summary:\ |