Remove library-specific code for `Import`.

Libraries are now handled like other modules.

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)