aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-04 14:46:52 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commit11ec801fa17434b0a3aad2c88a4422a22f1c4c44 (patch)
treef92521f724433aabe365cd4d20f585b1922e5860 /tools
parentb2b4e85ec6607d7364a0da9c65ae9303b9f73c03 (diff)
Put the list of Coq sources subdirectories in one place
and avoid duplication
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml8
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:\