From 2957e86c93556b0baf86b662d34fce1a2096edc2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 14:40:12 +0200
Subject: `do_modtype` -> `load_modtype`

---
 library/declaremods.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index eea129eae7..301e5a3431 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -233,7 +233,7 @@ let do_module' exists iter_objects i ((sp,kn),sobjs) =
 (** Nota: Interactive modules and module types cannot be recached!
     This used to be checked more properly here. *)
 
-let do_modtype i sp mp sobjs =
+let load_modtype i sp mp sobjs =
   if Nametab.exists_modtype sp then
     anomaly (pr_path sp ++ str " already exists.");
   Nametab.push_modtype (Nametab.Until i) sp mp;
@@ -247,7 +247,7 @@ let rec load_object i (name, obj) =
   | ModuleObject sobjs -> do_module' false load_objects i (name, sobjs)
   | ModuleTypeObject sobjs ->
     let (sp,kn) = name in
-    do_modtype i sp (mp_of_kn kn) sobjs
+    load_modtype i sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> load_include i (name, aobjs)
   | ImportObject _ -> ()
   | KeepObject objs -> load_keep i (name, objs)
@@ -326,7 +326,7 @@ let rec cache_object (name, obj) =
   | ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs)
   | ModuleTypeObject sobjs ->
     let (sp,kn) = name in
-    do_modtype 1 sp (mp_of_kn kn) sobjs
+    load_modtype 0 sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> cache_include (name, aobjs)
   | ImportObject { mp } -> really_import_module mp
   | KeepObject objs -> cache_keep (name, objs)
-- 
cgit v1.2.3


From 4614010ceddb9ed5100fa4e43d2807b172143a19 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 15:00:36 +0200
Subject: Specialize `ImportObject` to `Export`

`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
---
 library/declaremods.ml  | 16 ++++++++--------
 library/declaremods.mli | 11 +++--------
 library/lib.ml          |  9 +++------
 library/libobject.ml    |  2 +-
 library/libobject.mli   |  2 +-
 5 files changed, 16 insertions(+), 24 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 301e5a3431..50cf7245bc 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -110,9 +110,9 @@ and subst_objects subst seg =
     | IncludeObject aobjs ->
       let aobjs' = subst_aobjs subst aobjs in
       if aobjs' == aobjs then node else (id, IncludeObject aobjs')
-    | ImportObject { export; mp } ->
+    | ExportObject { mp } ->
       let mp' = subst_mp subst mp in
-      if mp'==mp then node else (id, ImportObject { export; mp = mp' })
+      if mp'==mp then node else (id, ExportObject { mp = mp' })
     | KeepObject _ -> assert false
   in
   List.Smart.map subst_one seg
@@ -249,7 +249,7 @@ let rec load_object i (name, obj) =
     let (sp,kn) = name in
     load_modtype i sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> load_include i (name, aobjs)
-  | ImportObject _ -> ()
+  | ExportObject _ -> ()
   | KeepObject objs -> load_keep i (name, objs)
 
 and load_objects i prefix objs =
@@ -289,7 +289,7 @@ and open_object i (name, obj) =
   | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs)
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
   | IncludeObject aobjs -> open_include i (name, aobjs)
-  | ImportObject { mp; _ } -> open_import i mp
+  | ExportObject { mp; _ } -> open_export i mp
   | KeepObject objs -> open_keep i (name, objs)
 
 and open_objects i prefix objs =
@@ -312,7 +312,7 @@ and open_include i ((sp,kn), aobjs) =
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
-and open_import i mp =
+and open_export i mp =
   if Int.equal i 1 then really_import_module mp
 
 and open_keep i ((sp,kn),kobjs) =
@@ -328,7 +328,7 @@ let rec cache_object (name, obj) =
     let (sp,kn) = name in
     load_modtype 0 sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> cache_include (name, aobjs)
-  | ImportObject { mp } -> really_import_module mp
+  | ExportObject { mp } -> really_import_module mp
   | KeepObject objs -> cache_keep (name, objs)
 
 and cache_include ((sp,kn), aobjs) =
@@ -975,9 +975,9 @@ let end_library ?except ~output_native_objects dir =
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
 
-let import_module export mp =
+let import_module ~export mp =
   really_import_module mp;
-  Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp }))
+  if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mp }))
 
 (** {6 Iterators} *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index ada53dbff0..c1d2de9783 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -103,18 +103,13 @@ val end_library :
 (** append a function to be executed at end_library *)
 val append_end_library_hook : (unit -> unit) -> unit
 
-(** [really_import_module mp] opens the module [mp] (in a Caml sense).
+(** [import_module export mp] imports the module [mp].
    It modifies Nametab and performs the [open_object] function for
    every object of the module. Raises [Not_found] when [mp] is unknown
-   or when [mp] corresponds to a functor. *)
-
-val really_import_module : ModPath.t -> unit
-
-(** [import_module export mp] is a synchronous version of
-   [really_import_module]. If [export] is [true], the module is also
+   or when [mp] corresponds to a functor. If [export] is [true], the module is also
    opened every time the module containing it is. *)
 
-val import_module : bool -> ModPath.t -> unit
+val import_module : export:bool -> ModPath.t -> unit
 
 (** Include  *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 3f51826315..851f086961 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -73,11 +73,8 @@ let classify_segment seg =
       clean ((id,o)::substl, keepl, anticipl) stk
     | KeepObject _ ->
       clean (substl, (id,o)::keepl, anticipl) stk
-    | ImportObject { export } ->
-      if export then
-        clean ((id,o)::substl, keepl, anticipl) stk
-      else
-        clean acc stk
+    | ExportObject _ ->
+      clean ((id,o)::substl, keepl, anticipl) stk
     | AtomicObject obj ->
       begin match classify_object obj with
         | Dispose -> clean acc stk
@@ -615,7 +612,7 @@ let discharge_item ((sp,_ as oname),e) =
   | Leaf lobj ->
     begin match lobj with
     | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
-    | ImportObject _ -> None
+    | ExportObject _ -> None
     | AtomicObject obj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj))
     end
diff --git a/library/libobject.ml b/library/libobject.ml
index 27e7810e6c..3d4a33c74e 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -75,7 +75,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ImportObject of { export : bool; mp : ModPath.t }
+  | ExportObject of { mp : ModPath.t }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
diff --git a/library/libobject.mli b/library/libobject.mli
index 3b37db4a6f..88d292ad03 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -112,7 +112,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ImportObject of { export : bool; mp : Names.ModPath.t }
+  | ExportObject of { mp : Names.ModPath.t }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
-- 
cgit v1.2.3


From 427065e815266084e4b03f7a2a75bf562eba775e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 15:48:12 +0200
Subject: Do not cache objects when importing modules

They have been already cached at loading time.
---
 library/declaremods.ml | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 50cf7245bc..0d74c55030 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -286,12 +286,26 @@ let rec really_import_module mp =
 and open_object i (name, obj) =
   match obj with
   | AtomicObject o -> Libobject.open_object i (name, o)
-  | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs)
+  | ModuleObject sobjs ->
+    let dir = dir_of_sp (fst name) in
+    let mp = mp_of_kn (snd name) in
+    open_module i dir mp sobjs
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
   | IncludeObject aobjs -> open_include i (name, aobjs)
   | ExportObject { mp; _ } -> open_export i mp
   | KeepObject objs -> open_keep i (name, objs)
 
+and open_module i obj_dir obj_mp sobjs =
+  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let dirinfo = Nametab.GlobDirRef.DirModule prefix in
+  consistency_checks true obj_dir dirinfo;
+  Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
+  (* If we're not a functor, let's iter on the internal components *)
+  if sobjs_no_functor sobjs then begin
+    let (prefix,objs,kobjs) = ModObjs.get obj_mp in
+    open_objects (i+1) prefix objs
+  end
+
 and open_objects i prefix objs =
   List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs
 
-- 
cgit v1.2.3


From a1abebc904e0931d896006fa67dc39bd1ca9e680 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 16:23:52 +0200
Subject: Optimize module Exports

This should compensate the removal of the library-level optimization,
while maintaining correct behavior.
---
 library/declaremods.ml | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0d74c55030..40c5178579 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -277,6 +277,29 @@ and load_keep i ((sp,kn),kobjs) =
 
 (** {6 Implementation of Import and Export commands} *)
 
+let mark_object obj (exports,acc) =
+  (exports, obj::acc)
+
+let rec collect_module_objects mp acc =
+  (* May raise Not_found for unknown module and for functors *)
+  let prefix,sobjs,keepobjs = ModObjs.get mp in
+  let acc = collect_objects 1 prefix keepobjs acc in
+  collect_objects 1 prefix sobjs acc
+
+and collect_object i (name, obj as o) acc =
+  match obj with
+  | ExportObject { mp; _ } -> collect_export i mp acc
+  | AtomicObject _ | IncludeObject _ | KeepObject _
+  | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
+
+and collect_objects i prefix objs acc =
+  List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc
+
+and collect_export i mp (exports,objs as acc) =
+  if Int.equal i 1 && not (MPset.mem mp exports) then
+    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 prefix,sobjs,keepobjs = ModObjs.get mp in
@@ -342,7 +365,7 @@ let rec cache_object (name, obj) =
     let (sp,kn) = name in
     load_modtype 0 sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> cache_include (name, aobjs)
-  | ExportObject { mp } -> really_import_module mp
+  | ExportObject { mp } -> anomaly Pp.(str "Export should not be cached")
   | KeepObject objs -> cache_keep (name, objs)
 
 and cache_include ((sp,kn), aobjs) =
@@ -990,7 +1013,8 @@ let end_library ?except ~output_native_objects dir =
   cenv,(substitute,keep),ast
 
 let import_module ~export mp =
-  really_import_module mp;
+  let _,objs = collect_module_objects mp (MPset.empty, []) in
+  List.iter (open_object 1) objs;
   if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mp }))
 
 (** {6 Iterators} *)
-- 
cgit v1.2.3


From 006a30ea6755230774bf22819b16807a95875329 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 6 Sep 2019 19:18:14 +0200
Subject: Turn `module_objects` into a record

---
 library/declaremods.ml | 52 ++++++++++++++++++++++++++++++++------------------
 1 file changed, 33 insertions(+), 19 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 40c5178579..e93d2c9481 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -151,7 +151,11 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs
      Module M:SIG. ... End M. have the keep list empty.
 *)
 
-type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects
+type module_objects =
+  { module_prefix : Nametab.object_prefix;
+    module_substituted_objects : Lib.lib_objects;
+    module_keep_objects : Lib.lib_objects;
+  }
 
 module ModObjs :
  sig
@@ -217,7 +221,13 @@ let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
   (* If we're not a functor, let's iter on the internal components *)
   if sobjs_no_functor sobjs then begin
     let objs = expand_sobjs sobjs in
-    ModObjs.set obj_mp (prefix,objs,kobjs);
+    let module_objects =
+      { module_prefix = prefix;
+        module_substituted_objects = objs;
+        module_keep_objects = kobjs;
+      }
+    in
+    ModObjs.set obj_mp module_objects;
     iter_objects (i+1) prefix objs;
     iter_objects (i+1) prefix kobjs
   end
@@ -266,13 +276,13 @@ and load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
   let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
   let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
-  let prefix',sobjs,kobjs0 =
+  let modobjs =
     try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
   in
-  assert Nametab.(eq_op prefix' prefix);
-  assert (List.is_empty kobjs0);
-  ModObjs.set obj_mp (prefix,sobjs,kobjs);
+  assert Nametab.(eq_op modobjs.module_prefix prefix);
+  assert (List.is_empty modobjs.module_keep_objects);
+  ModObjs.set obj_mp { modobjs with module_keep_objects = kobjs };
   load_objects i prefix kobjs
 
 (** {6 Implementation of Import and Export commands} *)
@@ -282,9 +292,10 @@ let mark_object obj (exports,acc) =
 
 let rec collect_module_objects mp acc =
   (* May raise Not_found for unknown module and for functors *)
-  let prefix,sobjs,keepobjs = ModObjs.get mp in
-  let acc = collect_objects 1 prefix keepobjs acc in
-  collect_objects 1 prefix sobjs acc
+  let modobjs = ModObjs.get mp in
+  let prefix = modobjs.module_prefix in
+  let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in
+  collect_objects 1 prefix modobjs.module_substituted_objects acc
 
 and collect_object i (name, obj as o) acc =
   match obj with
@@ -302,9 +313,10 @@ and collect_export i mp (exports,objs as acc) =
 
 let rec really_import_module mp =
   (* May raise Not_found for unknown module and for functors *)
-  let prefix,sobjs,keepobjs = ModObjs.get mp in
-  open_objects 1 prefix sobjs;
-  open_objects 1 prefix keepobjs
+  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) =
   match obj with
@@ -325,8 +337,8 @@ and open_module i obj_dir obj_mp sobjs =
   Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
   (* If we're not a functor, let's iter on the internal components *)
   if sobjs_no_functor sobjs then begin
-    let (prefix,objs,kobjs) = ModObjs.get obj_mp in
-    open_objects (i+1) prefix objs
+    let modobjs = ModObjs.get obj_mp in
+    open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects
   end
 
 and open_objects i prefix objs =
@@ -1026,9 +1038,10 @@ let iter_all_segments f =
       List.iter (apply_obj prefix) objs
     | _ -> f (Lib.make_oname prefix id) obj
   in
-  let apply_mod_obj _ (prefix,substobjs,keepobjs) =
-    List.iter (apply_obj prefix) substobjs;
-    List.iter (apply_obj prefix) keepobjs
+  let apply_mod_obj _ modobjs =
+    let prefix = modobjs.module_prefix in
+    List.iter (apply_obj prefix) modobjs.module_substituted_objects;
+    List.iter (apply_obj prefix) modobjs.module_keep_objects
   in
   let apply_node = function
     | sp, Lib.Leaf o -> f sp o
@@ -1054,9 +1067,10 @@ let debug_print_modtab _ =
     | [] -> str "[]"
     | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
-  let pr_modinfo mp (prefix,substobjs,keepobjs) s =
+  let pr_modinfo mp modobjs s =
+    let objs = modobjs.module_substituted_objects @ modobjs.module_keep_objects in
     s ++ str (ModPath.to_string mp) ++ (spc ())
-    ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs)))
+    ++ (pr_seg (Lib.segment_of_objects modobjs.module_prefix objs))
   in
   let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in
   hov 0 modules
-- 
cgit v1.2.3


From d1ccb99ef433a690be4d9d5289c7951c88925dd3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 10 Sep 2019 02:57:57 +0200
Subject: Optimize `Include`d `Export`s

---
 library/declaremods.ml | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3


From 24fc879cf2380bb28dd8c0f5ff8c7805ad121e1f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 12 Sep 2019 20:49:48 +0200
Subject: Optimize multiple imports

---
 library/declaremods.ml  | 35 +++++++++++++++++++++--------------
 library/declaremods.mli |  4 ++++
 library/libobject.ml    |  2 +-
 library/libobject.mli   |  2 +-
 4 files changed, 27 insertions(+), 16 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index cca3bfa3b7..b4dc42bdfe 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -110,9 +110,9 @@ and subst_objects subst seg =
     | IncludeObject aobjs ->
       let aobjs' = subst_aobjs subst aobjs in
       if aobjs' == aobjs then node else (id, IncludeObject aobjs')
-    | ExportObject { mp } ->
-      let mp' = subst_mp subst mp in
-      if mp'==mp then node else (id, ExportObject { mp = mp' })
+    | ExportObject { mpl } ->
+      let mpl' = List.map (subst_mp subst) mpl in
+      if mpl'==mpl then node else (id, ExportObject { mpl = mpl' })
     | KeepObject _ -> assert false
   in
   List.Smart.map subst_one seg
@@ -299,18 +299,23 @@ let rec collect_module_objects mp acc =
 
 and collect_object i (name, obj as o) acc =
   match obj with
-  | ExportObject { mp; _ } -> collect_export i mp acc
+  | ExportObject { mpl; _ } -> collect_export i mpl acc
   | AtomicObject _ | IncludeObject _ | KeepObject _
   | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
 
 and collect_objects i prefix objs acc =
   List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc
 
-and collect_export i mp (exports,objs as acc) =
-  if Int.equal i 1 && not (MPset.mem mp exports) then
+and collect_one_export mp (exports,objs as acc) =
+  if not (MPset.mem mp exports) then
     collect_module_objects mp (MPset.add mp exports, objs)
   else acc
 
+and collect_export i mpl acc =
+  if Int.equal i 1 then
+    List.fold_right collect_one_export mpl acc
+  else acc
+
 let rec open_object i (name, obj) =
   match obj with
   | AtomicObject o -> Libobject.open_object i (name, o)
@@ -320,7 +325,7 @@ let rec open_object i (name, obj) =
     open_module i dir mp sobjs
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
   | IncludeObject aobjs -> open_include i (name, aobjs)
-  | ExportObject { mp; _ } -> open_export i mp
+  | ExportObject { mpl; _ } -> open_export i mpl
   | KeepObject objs -> open_keep i (name, objs)
 
 and open_module i obj_dir obj_mp sobjs =
@@ -354,9 +359,8 @@ and open_include i ((sp,kn), aobjs) =
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
-and open_export i mp =
-  if Int.equal i 1 then
-  let _,objs = collect_module_objects mp (MPset.empty, []) in
+and open_export i mpl =
+  let _,objs = collect_export i mpl (MPset.empty, []) in
   List.iter (open_object 1) objs
 
 and open_keep i ((sp,kn),kobjs) =
@@ -372,7 +376,7 @@ let rec cache_object (name, obj) =
     let (sp,kn) = name in
     load_modtype 0 sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> cache_include (name, aobjs)
-  | ExportObject { mp } -> anomaly Pp.(str "Export should not be cached")
+  | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached")
   | KeepObject objs -> cache_keep (name, objs)
 
 and cache_include ((sp,kn), aobjs) =
@@ -1019,10 +1023,13 @@ let end_library ?except ~output_native_objects dir =
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
 
-let import_module ~export mp =
-  let _,objs = collect_module_objects mp (MPset.empty, []) in
+let import_modules ~export mpl =
+  let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in
   List.iter (open_object 1) objs;
-  if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mp }))
+  if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
+
+let import_module ~export mp =
+  import_modules ~export [mp]
 
 (** {6 Iterators} *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c1d2de9783..b7c7cd1dba 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -111,6 +111,10 @@ val append_end_library_hook : (unit -> unit) -> unit
 
 val import_module : export:bool -> ModPath.t -> unit
 
+(** Same as [import_module] but for multiple modules, and more optimized than
+    iterating [import_module]. *)
+val import_modules : export:bool -> ModPath.t list -> unit
+
 (** Include  *)
 
 val declare_include :
diff --git a/library/libobject.ml b/library/libobject.ml
index 3d4a33c74e..932f065f73 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -75,7 +75,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ExportObject of { mp : ModPath.t }
+  | ExportObject of { mpl : ModPath.t list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
diff --git a/library/libobject.mli b/library/libobject.mli
index 88d292ad03..146ccc293f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -112,7 +112,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ExportObject of { mp : Names.ModPath.t }
+  | ExportObject of { mpl : Names.ModPath.t list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
-- 
cgit v1.2.3