diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-21 20:10:26 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-23 12:50:45 +0100 |
commit | f4ee7ee31e4bc4a49de784d90b331abd3a21e34f (patch) | |
tree | ce42b1cbd9045d2f5b67435d1bd59fbba389b85b /library/library.ml | |
parent | 865c8cd9c3d6cd5dd91a86a26b81efe53bdf444a (diff) |
Fixing 934761875 about optimizing Import of several libraries at once (thanks to Enrico for noticing a bug).
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index e4169d66e..95b817d0a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -587,8 +587,11 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | m :: l -> - (match safe_locate_module m with + | (loc,dir as m) :: l -> + let m,acc = + try Nametab.locate_module dir, acc + with Not_found-> flush acc; safe_locate_module m, [] in + (match m with | MPfile dir -> aux (dir::acc) l | mp -> flush acc; Declaremods.import_module export mp; aux [] l) | [] -> flush acc |