diff options
| author | Maxime Dénès | 2019-09-10 02:57:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-16 09:56:58 +0200 |
| commit | d1ccb99ef433a690be4d9d5289c7951c88925dd3 (patch) | |
| tree | 4b16f11dd4d5e1e2f37a111b23241e452b5d91bd /library | |
| parent | 006a30ea6755230774bf22819b16807a95875329 (diff) | |
Optimize `Include`d `Export`s
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index e93d2c9481..cca3bfa3b7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -311,14 +311,7 @@ and collect_export i mp (exports,objs as acc) = collect_module_objects mp (MPset.add mp exports, objs) else acc -let rec really_import_module mp = - (* May raise Not_found for unknown module and for functors *) - let modobjs = ModObjs.get mp in - let prefix = modobjs.module_prefix in - open_objects 1 prefix modobjs.module_substituted_objects; - open_objects 1 prefix modobjs.module_keep_objects - -and open_object i (name, obj) = +let rec open_object i (name, obj) = match obj with | AtomicObject o -> Libobject.open_object i (name, o) | ModuleObject sobjs -> @@ -362,7 +355,9 @@ and open_include i ((sp,kn), aobjs) = open_objects i prefix o and open_export i mp = - if Int.equal i 1 then really_import_module mp + if Int.equal i 1 then + let _,objs = collect_module_objects mp (MPset.empty, []) in + List.iter (open_object 1) objs and open_keep i ((sp,kn),kobjs) = let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in |