aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 18:51:14 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 18:51:14 +0100
commit9daec838c8896e7c1048b42d01eba0c71c912f00 (patch)
treeb27a12e165d2c5b8c1b4d3171f961b8a5025bbb3
parentbff2b36cb0e2dbd02c4f181fba545a420e847767 (diff)
Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/checker.ml8
-rw-r--r--plugins/setoid_ring/newring.ml42
-rw-r--r--tools/coqdep.ml6
-rw-r--r--toplevel/coqinit.ml8
5 files changed, 7 insertions, 18 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 2663d8b55..8381144e8 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,6 +33,7 @@ Util
Ephemeron
Future
CUnix
+
Systemdirs
System
Profile
diff --git a/checker/checker.ml b/checker/checker.ml
index 263b8785a..360f99649 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -93,12 +93,6 @@ 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
@@ -124,7 +118,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_uppercase_subpaths ~unix_path:plugins ~coq_root:(Names.DirPath.make[coq_root]);
+ add_rec_path ~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 f040de33c..2f9e8509c 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 49693212d..57c9e82f2 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_uppercase_subdirs add_known "plugins" ["Coq"];
+ add_rec_dir add_known "plugins" ["Coq"];
add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
- add_rec_uppercase_subdirs (fun _ -> add_caml_known) "plugins" ["Coq"];
+ add_rec_dir (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_uppercase_subdirs add_coqlib_known (coqlib//"plugins") ["Coq"];
+ add_rec_dir 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 2d3418ce0..03074ced7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -71,12 +71,6 @@ 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
@@ -107,7 +101,7 @@ let init_load_path () =
(* then standard library *)
add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
(* then plugins *)
- add_stdlib_uppercase_subpaths ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:false;
+ add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
(* then user-contrib *)
if Sys.file_exists user_contrib then
add_userlib_path ~unix_path:user_contrib;