diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 9dc1dd5b..0b6fc48c 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -161,17 +161,6 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) -let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = - if exists_dir dir then - begin - add_ml_dir dir; - Loadpath.add_load_path dir - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_dirpath - end - else - msg_warning (str ("Cannot open " ^ dir)) - let convert_string d = try Names.Id.of_string d with UserError _ -> @@ -191,11 +180,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let dirs = List.map_filter convert_dirs dirs in let () = add_ml_dir unix_path in let add (path, dir) = - Loadpath.add_load_path path Loadpath.ImplicitPath dir in - let () = if implicit then List.iter add dirs in - Loadpath.add_load_path unix_path - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_root + Loadpath.add_load_path path ~implicit dir in + let () = List.iter add dirs in + Loadpath.add_load_path unix_path ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) |