diff options
| author | Maxime Dénès | 2019-09-12 20:49:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-16 09:56:59 +0200 |
| commit | 24fc879cf2380bb28dd8c0f5ff8c7805ad121e1f (patch) | |
| tree | eca5db1361318c4eb021f7e85ef8f892bd6f2373 /vernac | |
| parent | d1ccb99ef433a690be4d9d5289c7951c88925dd3 (diff) | |
Optimize multiple imports
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index 437ec7961e..8125c3de35 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -340,8 +340,7 @@ let load_require _ (_,(needed,modl,_)) = List.iter register_library needed let open_require i (_,(_,modl,export)) = - Option.iter (fun export -> List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modl) - export + Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export (* [needed] is the ordered list of libraries not already loaded *) let cache_require o = |