Merge PR #10476: Remove library-specific code for `Import`.

Reviewed-by: gares
Reviewed-by: ppedrot

19 files changed, 137 insertions, 217 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..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_bool; v_mp |];
+     [| List v_mp |];
      [| v_obj |]
   |])
 
@@ -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/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..10526a9ffe
--- /dev/null
+++ b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh
@@ -0,0 +1,10 @@
+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
+
+    vst_CI_REF=fix-export
+    vst_CI_GITURL=https://github.com/maximedenes/VST
+
+fi
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).
diff --git a/library/declaremods.ml b/library/declaremods.ml
index eea129eae7..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')
-    | ImportObject { export; mp } ->
-      let mp' = subst_mp subst mp in
-      if mp'==mp then node else (id, ImportObject { export; 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
@@ -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
@@ -233,7 +243,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,9 +257,9 @@ 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 _ -> ()
+  | ExportObject _ -> ()
   | KeepObject objs -> load_keep i (name, objs)
 
 and load_objects i prefix objs =
@@ -266,32 +276,69 @@ 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} *)
 
-let rec really_import_module mp =
+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
-  open_objects 1 prefix sobjs;
-  open_objects 1 prefix keepobjs
+  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
+  | 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_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
 
-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 -> 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)
-  | ImportObject { mp; _ } -> open_import i mp
+  | ExportObject { mpl; _ } -> open_export i mpl
   | 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 modobjs = ModObjs.get obj_mp in
+    open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects
+  end
+
 and open_objects i prefix objs =
   List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs
 
@@ -312,8 +359,9 @@ and open_include i ((sp,kn), aobjs) =
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
-and open_import i mp =
-  if Int.equal i 1 then really_import_module mp
+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) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
@@ -326,9 +374,9 @@ 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
+  | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached")
   | KeepObject objs -> cache_keep (name, objs)
 
 and cache_include ((sp,kn), aobjs) =
@@ -975,9 +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 =
-  really_import_module mp;
-  Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp }))
+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 { mpl }))
+
+let import_module ~export mp =
+  import_modules ~export [mp]
 
 (** {6 Iterators} *)
 
@@ -988,9 +1040,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
@@ -1016,9 +1069,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
diff --git a/library/declaremods.mli b/library/declaremods.mli
index ada53dbff0..b7c7cd1dba 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -103,18 +103,17 @@ 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
+
+(** 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  *)
 
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..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
-  | ImportObject of { export : bool; 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 3b37db4a6f..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
-  | ImportObject of { export : bool; mp : Names.ModPath.t }
+  | ExportObject of { mpl : Names.ModPath.t list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
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/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/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..8125c3de35 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,8 +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))
-    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 =
@@ -474,50 +378,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 export ->
+          List.iter (fun m -> Declaremods.import_module ~export (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 +413,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 +458,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..43b58d6d4b 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)