Capital letter in plugins.

5 files changed, 18 insertions, 7 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 8381144e8..2663d8b55 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,7 +33,6 @@ Util
 Ephemeron
 Future
 CUnix
-
 Systemdirs
 System
 Profile
diff --git a/checker/checker.ml b/checker/checker.ml
index 360f99649..263b8785a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -93,6 +93,12 @@ let add_rec_path ~unix_path ~coq_root =
   else
     msg_warning (str ("Cannot open " ^ unix_path))
 
+let add_rec_uppercase_subpaths ~unix_path ~coq_root =
+  Systemdirs.process_subdirectories (fun unix_path f ->
+    let id = Names.Id.of_string (String.capitalize f) in
+    let coq_root = DirPath.make (id :: DirPath.repr coq_root) in
+    add_rec_path ~unix_path ~coq_root) unix_path
+
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
@@ -118,7 +124,7 @@ let init_load_path () =
   (* first standard library *)
   add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]);
   (* then plugins *)
-  add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]);
+  add_rec_uppercase_subpaths ~unix_path:plugins ~coq_root:(Names.DirPath.make[coq_root]);
   (* then user-contrib *)
   if Sys.file_exists user_contrib then
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509c..f040de33c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -260,7 +260,7 @@ let rec dest_rel t =
 (****************************************************************************)
 (* Library linking *)
 
-let plugin_dir = "setoid_ring"
+let plugin_dir = "Setoid_ring"
 
 let cdir = ["Coq";plugin_dir]
 let plugin_modules =
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 57c9e82f2..49693212d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -482,14 +482,14 @@ let coqdep () =
   (* NOTE: These directories are searched from last to first *)
   if !option_boot then begin
     add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"];
+    add_rec_uppercase_subdirs add_known "plugins" ["Coq"];
     add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
+    add_rec_uppercase_subdirs (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
     Envars.set_coqlib ~fail:Errors.error;
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
-    add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
+    add_rec_uppercase_subdirs add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_dir add_coqlib_known user [];
     List.iter (fun s -> add_dir add_coqlib_known s [])
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 03074ced7..2d3418ce0 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -71,6 +71,12 @@ let add_stdlib_path ~unix_path ~coq_root ~with_ml =
   if with_ml then
     Mltop.add_rec_ml_dir unix_path
 
+let add_stdlib_uppercase_subpaths ~unix_path ~coq_root ~with_ml =
+  Systemdirs.process_subdirectories (fun unix_path f ->
+    let id = Names.Id.of_string (String.capitalize f) in
+    let coq_root = Libnames.add_dirpath_suffix coq_root id in
+    add_stdlib_path ~unix_path ~coq_root ~with_ml) unix_path
+
 let add_userlib_path ~unix_path =
   Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
   Mltop.add_rec_ml_dir unix_path
@@ -101,7 +107,7 @@ let init_load_path () =
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
-    add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
+    add_stdlib_uppercase_subpaths ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:false;
     (* then user-contrib *)
     if Sys.file_exists user_contrib then
       add_userlib_path ~unix_path:user_contrib;