diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 9dc1dd5b1..357c5482f 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -165,9 +165,7 @@ 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 + Loadpath.add_load_path dir ~root:true ~implicit coq_dirpath end else msg_warning (str ("Cannot open " ^ dir)) @@ -191,11 +189,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 ~root:false ~implicit dir in + let () = List.iter add dirs in + Loadpath.add_load_path unix_path ~root:true ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) |