diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 458fe8ef0..196ab98ed 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -180,7 +180,6 @@ let add_rec_path ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in let () = add_ml_dir unix_path in let add (path, dir) = Loadpath.add_load_path path Loadpath.ImplicitPath dir in |