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