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`.

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