diff options
| author | Hugo Herbelin | 2015-02-01 15:11:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-12 17:20:35 +0100 |
| commit | bff2b36cb0e2dbd02c4f181fba545a420e847767 (patch) | |
| tree | af281e4201f2e1cbee3aaf6c2d1d07fadbc9b4be /toplevel | |
| parent | 5268efdefb396267bfda0c17eb045fa2ed516b3c (diff) | |
Capital letter in plugins.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced70..2d3418ce02 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; |