Put the list of Coq sources subdirectories in one place

and avoid duplication

4 files changed, 14 insertions, 15 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 330b0fbd6..b20d39fb5 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,8 +146,6 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-
 let ocamlfind () =
   if !Flags.ocamlfind_spec then !Flags.ocamlfind else
     if !Flags.boot then Coq_config.ocamlfind else
@@ -210,6 +208,13 @@ let xdg_dirs ~warn =
 
 (* Print the configuration information *)
 
+let coq_src_subdirs = [ 
+   "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
+   "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
+   "tactics" ; "toplevel" ; "printing" ; "intf" ;
+   "grammar" ; "ide" ; "stm"; "vernac" ] @
+   Coq_config.plugins_dirs
+  
 let print_config f =
   let open Printf in 
   fprintf f "LOCAL=%s\n" (if Coq_config.local then "1" else "0");
@@ -222,3 +227,4 @@ let print_config f =
   fprintf f "CAMLP4LIB=%s\n" (camlp4lib ());
   fprintf f "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
   fprintf f "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")
+
diff --git a/lib/envars.mli b/lib/envars.mli
index b9cc534f9..d158407b4 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -72,3 +72,6 @@ val xdg_dirs : warn : (string -> unit) -> string list
 
 (** {6 Prints the configuration information } *)
 val print_config : out_channel -> unit
+
+(** Directories in which coq sources are found *)
+val coq_src_subdirs : string list
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:\
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 2b9a04dad..8fca30268 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -121,14 +121,10 @@ let init_library_roots () =
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
   let add_subdir dl =
-    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl)
+    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
   in
     Mltop.add_ml_dir (Envars.coqlib ());
-    List.iter add_subdir
-      [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
-	[ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-	[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
-        [ "grammar" ]; [ "ide" ]; [ "ltac" ]; [ "vernac" ]; ]
+    List.iter add_subdir Envars.coq_src_subdirs
 
 let get_compat_version = function
   | "8.7" -> Flags.Current