From 181597904ae9211facaa406371b5d54d61f40cbf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Jul 2019 10:16:26 +0200
Subject: Remove library-specific code for `Import`.

Libraries are now handled like other modules.
---
 checker/check.ml                  |   1 -
 checker/values.ml                 |   2 +-
 plugins/btauto/Algebra.v          |   2 +-
 plugins/setoid_ring/Cring.v       |   1 +
 test-suite/bugs/closed/bug_3481.v |   1 -
 test-suite/bugs/closed/bug_4498.v |   3 +-
 test-suite/success/Nsatz.v        |   2 +-
 theories/Reals/Machin.v           |   2 +-
 vernac/library.ml                 | 145 ++------------------------------------
 vernac/library.mli                |  11 +--
 vernac/vernacentries.ml           |  20 +++---
 11 files changed, 23 insertions(+), 167 deletions(-)

diff --git a/checker/check.ml b/checker/check.ml
index ecf84fda9c..69de2536c5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -262,7 +262,6 @@ let raw_intern_library f =
 
 type summary_disk = {
   md_name : compilation_unit_name;
-  md_imports : compilation_unit_name array;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
 }
 
diff --git a/checker/values.ml b/checker/values.ml
index cc9ac1f834..708419e7cc 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -395,7 +395,7 @@ let v_stm_seg = v_pair v_tasks v_counters
 (** Toplevel structures in a vo (see Cic.mli) *)
 
 let v_libsum =
-  Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+  Tuple ("summary", [|v_dp;v_deps|])
 
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 638a4cef21..3ad5bc9f2d 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Omega Lia.
+Require Import Bool PArith DecidableClass Ring Omega Lia.
 
 Ltac bool :=
 repeat match goal with
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 4f3f0c3878..df0313a624 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -19,6 +19,7 @@ Require Export Algebra_syntax.
 Require Export Ncring.
 Require Export Ncring_initial.
 Require Export Ncring_tac.
+Require Import InitialRing.
 
 Class Cring {R:Type}`{Rr:Ring R} := 
  cring_mul_comm: forall x y:R, x * y == y * x.
diff --git a/test-suite/bugs/closed/bug_3481.v b/test-suite/bugs/closed/bug_3481.v
index 41e1a8e959..f54810d359 100644
--- a/test-suite/bugs/closed/bug_3481.v
+++ b/test-suite/bugs/closed/bug_3481.v
@@ -1,7 +1,6 @@
 
 Set Implicit Arguments.
 
-Require Import Logic.
 Module NonPrim.
 Local Set Nonrecursive Elimination Schemes.
 Record prodwithlet (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 9b3210860c..ba63b707af 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -1,6 +1,7 @@
 Require Export Coq.Unicode.Utf8.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Relations.Relation_Definitions.
+Require Export Coq.Setoids.Setoid.
 
 Set Universe Polymorphism.
 
@@ -17,8 +18,6 @@ Class Category := {
       Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
 }.
 
-Require Export Coq.Setoids.Setoid.
-
 Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index e38affd7fa..381fbabe72 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -58,8 +58,8 @@ Section Geometry.
    https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr
 *)
 
-Require Import List.
 Require Import Reals.
+Require Import List.
 
 Record point:Type:={
  X:R;
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 81f8b08c92..08bc38a085 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+Require Import Omega.
 Require Import Lra.
 Require Import Rbase.
 Require Import Rtrigo1.
@@ -18,7 +19,6 @@ Require Import Rseries.
 Require Import SeqProp.
 Require Import PartSum.
 Require Import Ratan.
-Require Import Omega.
 
 Local Open Scope R_scope.
 
diff --git a/vernac/library.ml b/vernac/library.ml
index e91cb965f5..ed29ebecd3 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 
 open Names
-open Libnames
 open Lib
 open Libobject
 
@@ -85,7 +84,6 @@ type library_disk = {
 
 type summary_disk = {
   md_name : compilation_unit_name;
-  md_imports : compilation_unit_name array;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
 }
 
@@ -96,7 +94,6 @@ type library_t = {
   library_name : compilation_unit_name;
   library_data : library_disk delayed;
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
-  library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
   library_extra_univs : Univ.ContextSet.t;
 }
@@ -104,7 +101,6 @@ type library_t = {
 type library_summary = {
   libsum_name : compilation_unit_name;
   libsum_digests : Safe_typing.vodigest;
-  libsum_imports : compilation_unit_name array;
 }
 
 module LibraryOrdered = DirPath
@@ -121,8 +117,6 @@ let libraries_filename_table = ref LibraryFilenameMap.empty
 
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
 let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
-let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
-let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
 
 (* various requests to the tables *)
 
@@ -155,13 +149,6 @@ let library_is_loaded dir =
   try let _ = find_library dir in true
   with Not_found -> false
 
-let library_is_opened dir =
-  List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list
-
-let loaded_libraries () = !libraries_loaded_list
-
-let opened_libraries () = !libraries_imports_list
-
   (* If a library is loaded several time, then the first occurrence must
      be performed first, thus the libraries_loaded_list ... *)
 
@@ -182,87 +169,7 @@ let register_loaded_library m =
   libraries_loaded_list := aux !libraries_loaded_list;
   libraries_table := LibraryMap.add libname m !libraries_table
 
-  (* ... while if a library is imported/exported several time, then
-     only the last occurrence is really needed - though the imported
-     list may differ from the exported list (consider the sequence
-     Export A; Export B; Import A which results in A;B for exports but
-     in B;A for imports) *)
-
-let rec remember_last_of_each l m =
-  match l with
-  | [] -> [m]
-  | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m
-  | m'::l' -> m' :: remember_last_of_each l' m
-
-let register_open_library export m =
-  libraries_imports_list := remember_last_of_each !libraries_imports_list m;
-  if export then
-    libraries_exports_list := remember_last_of_each !libraries_exports_list m
-
-(************************************************************************)
-(*s Opening libraries *)
-
-(* [open_library export explicit m] opens library [m] if not already
-   opened _or_ if explicitly asked to be (re)opened *)
-
-let open_library export explicit_libs m =
-  if
-    (* Only libraries indirectly to open are not reopen *)
-    (* Libraries explicitly mentioned by the user are always reopen *)
-    List.exists (fun m' -> DirPath.equal m m') explicit_libs
-    || not (library_is_opened m)
-  then begin
-    register_open_library export m;
-    Declaremods.really_import_module (MPfile m)
-  end
-  else
-    if export then
-      libraries_exports_list := remember_last_of_each !libraries_exports_list m
-
-(* open_libraries recursively open a list of libraries but opens only once
-   a library that is re-exported many times *)
-
-let open_libraries export modl =
-  let to_open_list =
-    List.fold_left
-      (fun l m ->
-         let subimport =
-           Array.fold_left
-             (fun l m -> remember_last_of_each l m)
-             l m.libsum_imports
-         in remember_last_of_each subimport m.libsum_name)
-      [] modl in
-  let explicit = List.map (fun m -> m.libsum_name) modl in
-  List.iter (open_library export explicit) to_open_list
-
-
-(**********************************************************************)
-(* import and export of libraries - synchronous operations            *)
-(* at the end similar to import and export of modules except that it  *)
-(* is optimized: when importing several libraries at the same time    *)
-(* which themselves indirectly imports the very same modules, these   *)
-(* ones are imported only ones *)
-
-let open_import_library i (_,(modl,export)) =
-  if Int.equal i 1 then
-    (* even if the library is already imported, we re-import it *)
-    (* if not (library_is_opened dir) then *)
-      open_libraries export (List.map try_find_library modl)
-
-let cache_import_library obj =
-  open_import_library 1 obj
-
-let subst_import_library (_,o) = o
-
-let classify_import_library (_,export as obj) =
-  if export then Substitute obj else Dispose
-
-let in_import_library : DirPath.t list * bool -> obj =
-  declare_object {(default_object "IMPORT LIBRARY") with
-       cache_function = cache_import_library;
-       open_function = open_import_library;
-       subst_function = subst_import_library;
-       classify_function = classify_import_library }
+  let loaded_libraries () = !libraries_loaded_list
 
 (************************************************************************)
 (** {6 Tables of opaque proof terms} *)
@@ -327,14 +234,12 @@ let mk_library sd md digests univs =
     library_name     = sd.md_name;
     library_data     = md;
     library_deps     = sd.md_deps;
-    library_imports  = sd.md_imports;
     library_digests  = digests;
     library_extra_univs = univs;
   }
 
 let mk_summary m = {
   libsum_name = m.library_name;
-  libsum_imports = m.library_imports;
   libsum_digests = m.library_digests;
 }
 
@@ -435,7 +340,7 @@ let load_require _ (_,(needed,modl,_)) =
   List.iter register_library needed
 
 let open_require i (_,(_,modl,export)) =
-  Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
+  Option.iter (fun exp -> List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modl)
     export
 
   (* [needed] is the ordered list of libraries not already loaded *)
@@ -474,50 +379,15 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
     if Lib.is_module_or_modtype () then
       begin
         warn_require_in_module ();
-        add_anonymous_leaf (in_require (needed,modrefl,None));
-        Option.iter (fun exp ->
-          add_anonymous_leaf (in_import_library (modrefl,exp)))
-          export
+              add_anonymous_leaf (in_require (needed,modrefl,None));
+              Option.iter (fun exp ->
+          List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modrefl)
+                export
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
   ()
 
-(* the function called by Vernacentries.vernac_import *)
-
-let safe_locate_module qid =
-  try Nametab.locate_module qid
-  with Not_found ->
-    user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module"
-      (pr_qualid qid ++ str " is not a module")
-
-let import_module export modl =
-  (* Optimization: libraries in a raw in the list are imported
-     "globally".  If there is non-library in the list; it breaks the
-     optimization For instance: "Import Arith MyModule Zarith" will
-     not be optimized (possibly resulting in redefinitions, but
-     "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule"
-     will have the submodules imported by both Arith and ZArith
-     imported only once *)
-  let flush = function
-    | [] -> ()
-    | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
-  let rec aux acc = function
-    | qid :: l ->
-        let m,acc =
-          try Nametab.locate_module qid, acc
-          with Not_found-> flush acc; safe_locate_module qid, [] in
-        (match m with
-        | MPfile dir -> aux (dir::acc) l
-        | mp ->
-            flush acc;
-            try Declaremods.import_module export mp; aux [] l
-            with Not_found ->
-              user_err ?loc:qid.CAst.loc ~hdr:"import_module"
-                (pr_qualid qid ++ str " is not a module"))
-    | [] -> flush acc
-  in aux [] modl
-
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
@@ -544,8 +414,6 @@ let current_deps () =
   in
   List.map map !libraries_loaded_list
 
-let current_reexports () = !libraries_exports_list
-
 let error_recursively_dependent_library dir =
   user_err
     (strbrk "Unable to use logical name " ++ DirPath.print dir ++
@@ -591,7 +459,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
-    md_imports = Array.of_list (current_reexports ());
   } in
   let md = {
     md_compiled = cenv;
diff --git a/vernac/library.mli b/vernac/library.mli
index 973b369226..6a32413248 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Libnames
 
 (** This module provides functions to load, open and save
   libraries. Libraries correspond to the subclass of modules that
@@ -37,10 +36,6 @@ type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
 type seg_proofs = Opaqueproof.opaque_proofterm array
 
-(** Open a module (or a library); if the boolean is true then it's also
-   an export otherwise just a simple import *)
-val import_module : bool -> qualid list -> unit
-
 (** End the compilation of a library and save it to a ".vo" file.
     [output_native_objects]: when producing vo objects, also compile the native-code version. *)
 val save_library_to :
@@ -56,13 +51,11 @@ val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs ->
 
 (** {6 Interrogate the status of libraries } *)
 
-  (** - Tell if a library is loaded or opened *)
+  (** - Tell if a library is loaded *)
 val library_is_loaded : DirPath.t -> bool
-val library_is_opened : DirPath.t -> bool
 
-  (** - Tell which libraries are loaded or imported *)
+  (** - Tell which libraries are loaded *)
 val loaded_libraries : unit -> DirPath.t list
-val opened_libraries : unit -> DirPath.t list
 
   (** - Return the full filename of a loaded library. *)
 val library_full_filename : DirPath.t -> string
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3d14e8d510..adfe469811 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -171,16 +171,9 @@ let print_loadpath dir =
     prlist_with_sep fnl Loadpath.pp l
 
 let print_modules () =
-  let opened = Library.opened_libraries ()
-  and loaded = Library.loaded_libraries () in
-  (* we intersect over opened to preserve the order of opened since *)
-  (* non-commutative operations (e.g. visibility) are done at import time *)
-  let loaded_opened = List.intersect DirPath.equal opened loaded
-  and only_loaded = List.subtract DirPath.equal loaded opened in
-  str"Loaded and imported library files: " ++
-  pr_vertical_list DirPath.print loaded_opened ++ fnl () ++
-  str"Loaded and not imported library files: " ++
-  pr_vertical_list DirPath.print only_loaded
+  let loaded = Library.loaded_libraries () in
+  str"Loaded library files: " ++
+  pr_vertical_list DirPath.print loaded
 
 
 let print_module qid =
@@ -862,7 +855,12 @@ let vernac_constraint ~poly l =
 (* Modules            *)
 
 let vernac_import export refl =
-  Library.import_module export refl
+  let import_mod qid =
+    try Declaremods.import_module export @@ Nametab.locate_module qid
+    with Not_found ->
+      CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
+   in
+  List.iter import_mod refl
 
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
-- 
cgit v1.2.3


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(-)

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`.
---
 checker/values.ml       |  2 +-
 library/declaremods.ml  | 16 ++++++++--------
 library/declaremods.mli | 11 +++--------
 library/lib.ml          |  9 +++------
 library/libobject.ml    |  2 +-
 library/libobject.mli   |  2 +-
 printing/printmod.ml    |  2 +-
 vernac/library.ml       |  6 +++---
 vernac/vernacentries.ml |  2 +-
 9 files changed, 22 insertions(+), 30 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 708419e7cc..1590097731 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| v_bool; v_mp |];
+     [| v_mp |];
      [| v_obj |]
   |])
 
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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 43992ec9d3..141469ff9c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -242,7 +242,7 @@ let nametab_register_body mp dir (l,body) =
 
 let nametab_register_module_body mp struc =
   (* If [mp] is a globally visible module, we simply import it *)
-  try Declaremods.really_import_module mp
+  try Declaremods.import_module ~export:false mp
   with Not_found ->
     (* Otherwise we try to emulate an import by playing with nametab *)
     nametab_register_dir mp;
diff --git a/vernac/library.ml b/vernac/library.ml
index ed29ebecd3..437ec7961e 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -340,7 +340,7 @@ let load_require _ (_,(needed,modl,_)) =
   List.iter register_library needed
 
 let open_require i (_,(_,modl,export)) =
-  Option.iter (fun exp -> List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modl)
+  Option.iter (fun export -> List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modl)
     export
 
   (* [needed] is the ordered list of libraries not already loaded *)
@@ -380,8 +380,8 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
       begin
         warn_require_in_module ();
               add_anonymous_leaf (in_require (needed,modrefl,None));
-              Option.iter (fun exp ->
-          List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modrefl)
+        Option.iter (fun export ->
+          List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl)
                 export
       end
     else
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index adfe469811..43b58d6d4b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -856,7 +856,7 @@ let vernac_constraint ~poly l =
 
 let vernac_import export refl =
   let import_mod qid =
-    try Declaremods.import_module export @@ Nametab.locate_module qid
+    try Declaremods.import_module ~export @@ Nametab.locate_module qid
     with Not_found ->
       CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
    in
-- 
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(-)

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(-)

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 ebae43ef801ae282592285f5800289c1d6398657 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 5 Sep 2019 17:22:40 +0200
Subject: Add SF overlay

---
 dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh

diff --git a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
new file mode 100644
index 0000000000..0a9fc29c6d
--- /dev/null
+++ b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "10476" ] || [ "$CI_BRANCH" = "rm-library-optim" ]; then
+
+    sf_lf_CI_TARURL=https://www.maximedenes.fr/download/lf.tgz
+    sf_plf_CI_TARURL=https://www.maximedenes.fr/download/plf.tgz
+    sf_vfa_CI_TARURL=https://www.maximedenes.fr/download/vfa.tgz
+
+fi
-- 
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(-)

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(-)

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

---
 checker/values.ml       |  2 +-
 library/declaremods.ml  | 35 +++++++++++++++++++++--------------
 library/declaremods.mli |  4 ++++
 library/libobject.ml    |  2 +-
 library/libobject.mli   |  2 +-
 vernac/library.ml       |  3 +--
 6 files changed, 29 insertions(+), 19 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 1590097731..6b340635d7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| v_mp |];
+     [| List v_mp |];
      [| v_obj |]
   |])
 
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
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 =
-- 
cgit v1.2.3


From a5fde0dec78e7d9f1747a43ac3805a32490e57e5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Sep 2019 08:00:16 +0200
Subject: Overlay for VST

---
 dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
index 0a9fc29c6d..10526a9ffe 100644
--- a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
+++ b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
@@ -4,4 +4,7 @@ if [ "$CI_PULL_REQUEST" = "10476" ] || [ "$CI_BRANCH" = "rm-library-optim" ]; th
     sf_plf_CI_TARURL=https://www.maximedenes.fr/download/plf.tgz
     sf_vfa_CI_TARURL=https://www.maximedenes.fr/download/vfa.tgz
 
+    vst_CI_REF=fix-export
+    vst_CI_GITURL=https://github.com/maximedenes/VST
+
 fi
-- 
cgit v1.2.3


From 73b9794cc21e9fe932d5be9836fe1c53659ba717 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Sep 2019 08:00:35 +0200
Subject: Add changelog entry

---
 doc/changelog/07-commands-and-options/10476-fix-export.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/10476-fix-export.rst

diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst
new file mode 100644
index 0000000000..ba71e1c337
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10476-fix-export.rst
@@ -0,0 +1,5 @@
+- Fix two bugs in `Export`. This can have an impact on the behavior of the
+  `Import` command on libraries. `Import A` when `A` imports `B` which exports
+  `C` was importing `C`, whereas `Import` is not transitive. Also, after
+  `Import A B`, the import of `B` was sometimes incomplete.
+  (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès).
-- 
cgit v1.2.3