Merge PR #11820: Partial imports

Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot

13 files changed, 200 insertions, 89 deletions

diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 390ed62bee..eaa6c84791 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -28,7 +28,7 @@ let discharge_canonical_structure (_,((gref, _ as x), local)) =
 
 let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
-                  open_function = open_canonical_structure;
+                  open_function = simple_open open_canonical_structure;
                   cache_function = cache_canonical_structure;
                   subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
                   classify_function = (fun x -> Substitute x);
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d38713e09..a9425b15d2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,7 +116,7 @@ let instance_input : instance -> obj =
     { (default_object "type classes instances state") with
       cache_function = cache_instance;
       load_function = (fun _ x -> cache_instance x);
-      open_function = (fun _ x -> cache_instance x);
+      open_function = simple_open (fun _ x -> cache_instance x);
       classify_function = classify_instance;
       discharge_function = discharge_instance;
       rebuild_function = rebuild_instance;
@@ -237,7 +237,7 @@ let class_input : typeclass -> obj =
     { (default_object "type classes state") with
       cache_function = cache_class;
       load_function = (fun _ -> cache_class);
-      open_function = (fun _ -> cache_class);
+      open_function = simple_open (fun _ -> cache_class);
       classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index c339c53a9b..4a8e217fc1 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -256,7 +256,7 @@ let classify_coercion obj =
 
 let inCoercion : coercion -> obj =
   declare_object {(default_object "COERCION") with
-    open_function = open_coercion;
+    open_function = simple_open open_coercion;
     cache_function = cache_coercion;
     subst_function = (fun (subst,c) -> subst_coercion subst c);
     classify_function = classify_coercion;
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2610f16d92..3e6552c8d2 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -49,9 +49,12 @@ let load_inductive i ((sp, kn), names) =
   let names = inductive_names sp kn names in
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
 
-let open_inductive i ((sp, kn), names) =
+let open_inductive f i ((sp, kn), names) =
   let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+  List.iter (fun (sp, ref) ->
+      if Libobject.in_filter_ref ref f then
+        Nametab.push (Nametab.Exactly i) sp ref)
+    names
 
 let cache_inductive ((sp, kn), names) =
   let names = inductive_names sp kn names in
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 300dfe6c35..20fa43c8e7 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -56,7 +56,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
     { (default_object "Global universe name state") with
       cache_function = cache_univ_names;
       load_function = load_univ_names;
-      open_function = open_univ_names;
+      open_function = simple_open open_univ_names;
       discharge_function = discharge_univ_names;
       subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 4f527b73d0..438509e28a 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -81,6 +81,19 @@ module ModSubstObjs :
 
 let sobjs_no_functor (mbids,_) = List.is_empty mbids
 
+let subst_filtered sub (f,mp) =
+  let f = match f with
+    | Unfiltered -> Unfiltered
+    | Names ns ->
+      let module NSet = Globnames.ExtRefSet in
+      let ns =
+        NSet.fold (fun n ns -> NSet.add (Globnames.subst_extended_reference sub n) ns)
+          ns NSet.empty
+      in
+      Names ns
+  in
+  f, subst_mp sub mp
+
 let rec subst_aobjs sub = function
   | Objs o as objs ->
     let o' = subst_objects sub o in
@@ -109,7 +122,7 @@ and subst_objects subst seg =
       let aobjs' = subst_aobjs subst aobjs in
       if aobjs' == aobjs then node else (id, IncludeObject aobjs')
     | ExportObject { mpl } ->
-      let mpl' = List.map (subst_mp subst) mpl in
+      let mpl' = List.Smart.map (subst_filtered subst) mpl in
       if mpl'==mpl then node else (id, ExportObject { mpl = mpl' })
     | KeepObject _ -> assert false
   in
@@ -285,86 +298,103 @@ and load_keep i ((sp,kn),kobjs) =
 
 (** {6 Implementation of Import and Export commands} *)
 
-let mark_object obj (exports,acc) =
-  (exports, obj::acc)
+let mark_object f obj (exports,acc) =
+  (exports, (f,obj)::acc)
 
-let rec collect_module_objects mp acc =
+let rec collect_module_objects (f,mp) acc =
   (* May raise Not_found for unknown module and for functors *)
   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
+  let acc = collect_objects f 1 prefix modobjs.module_keep_objects acc in
+  collect_objects f 1 prefix modobjs.module_substituted_objects acc
 
-and collect_object i (name, obj as o) acc =
+and collect_object f i (name, obj as o) acc =
   match obj with
-  | ExportObject { mpl; _ } -> collect_export i mpl acc
+  | ExportObject { mpl } -> collect_export f i mpl acc
   | AtomicObject _ | IncludeObject _ | KeepObject _
-  | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
+  | ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
+
+and collect_objects f i prefix objs acc =
+  List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+
+and collect_one_export f (f',mp) (exports,objs as acc) =
+  match filter_and f f' with
+  | None -> acc
+  | Some f ->
+    let exports' = MPmap.update mp (function
+        | None -> Some f
+        | Some f0 -> Some (filter_or f f0))
+        exports
+    in
+    (* If the map doesn't change there is nothing new to export.
 
-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
+       It's possible that [filter_and] or [filter_or] mangled precise
+       filters such that we repeat uselessly, but the important
+       [Unfiltered] case is handled correctly.
+    *)
+    if exports == exports' then acc
+    else
+      collect_module_objects (f,mp) (exports', objs)
 
-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 =
+and collect_export f i mpl acc =
   if Int.equal i 1 then
-    List.fold_right collect_one_export mpl acc
+    List.fold_right (collect_one_export f) mpl acc
   else acc
 
-let rec open_object i (name, obj) =
+let open_modtype i ((sp,kn),_) =
+  let mp = mp_of_kn kn in
+  let mp' =
+    try Nametab.locate_modtype (qualid_of_path sp)
+    with Not_found ->
+      anomaly (pr_path sp ++ str " should already exist!");
+  in
+  assert (ModPath.equal mp mp');
+  Nametab.push_modtype (Nametab.Exactly i) sp mp
+
+let rec open_object f i (name, obj) =
   match obj with
-  | AtomicObject o -> Libobject.open_object i (name, o)
+  | AtomicObject o -> Libobject.open_object f i (name, o)
   | ModuleObject sobjs ->
     let dir = dir_of_sp (fst name) in
     let mp = mp_of_kn (snd name) in
-    open_module i dir mp sobjs
+    open_module f i dir mp sobjs
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
-  | IncludeObject aobjs -> open_include i (name, aobjs)
-  | ExportObject { mpl; _ } -> open_export i mpl
-  | KeepObject objs -> open_keep i (name, objs)
+  | IncludeObject aobjs -> open_include f i (name, aobjs)
+  | ExportObject { mpl } -> open_export f i mpl
+  | KeepObject objs -> open_keep f i (name, objs)
 
-and open_module i obj_dir obj_mp sobjs =
+and open_module f i obj_dir obj_mp sobjs =
   let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks true obj_dir dirinfo;
-  Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
+  (match f with
+   | Unfiltered -> Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo
+   | Names _ -> ());
   (* 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
+    open_objects f (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
-
-and open_modtype i ((sp,kn),_) =
-  let mp = mp_of_kn kn in
-  let mp' =
-    try Nametab.locate_modtype (qualid_of_path sp)
-    with Not_found ->
-      anomaly (pr_path sp ++ str " should already exist!");
-  in
-  assert (ModPath.equal mp mp');
-  Nametab.push_modtype (Nametab.Exactly i) sp mp
+and open_objects f i prefix objs =
+  List.iter (fun (id, obj) -> open_object f i (Lib.make_oname prefix id, obj)) objs
 
-and open_include i ((sp,kn), aobjs) =
+and open_include f i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
   let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
-  open_objects i prefix o
+  open_objects f i prefix o
 
-and open_export i mpl =
-  let _,objs = collect_export i mpl (MPset.empty, []) in
-  List.iter (open_object 1) objs
+and open_export f i mpl =
+  let _,objs = collect_export f i mpl (MPmap.empty, []) in
+  List.iter (fun (f,o) -> open_object f 1 o) objs
 
-and open_keep i ((sp,kn),kobjs) =
+and open_keep f i ((sp,kn),kobjs) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
   let prefix = Nametab.{ obj_dir; obj_mp; } in
-  open_objects i prefix kobjs
+  open_objects f i prefix kobjs
 
 let rec cache_object (name, obj) =
   match obj with
@@ -383,7 +413,7 @@ and cache_include ((sp,kn), aobjs) =
   let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects 1 prefix o;
-  open_objects 1 prefix o
+  open_objects Unfiltered 1 prefix o
 
 and cache_keep ((sp,kn),kobjs) =
   anomaly (Pp.str "This module should not be cached!")
@@ -1023,12 +1053,12 @@ let end_library ?except ~output_native_objects dir =
   cenv,(substitute,keep),ast
 
 let import_modules ~export mpl =
-  let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in
-  List.iter (open_object 1) objs;
+  let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+  List.iter (fun (f,o) -> open_object f 1 o) objs;
   if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
 
-let import_module ~export mp =
-  import_modules ~export [mp]
+let import_module f ~export mp =
+  import_modules ~export [f,mp]
 
 (** {6 Iterators} *)
 
@@ -1073,6 +1103,6 @@ let debug_print_modtab _ =
 
 
 let mod_ops = {
-  Printmod.import_module = import_module;
+  Printmod.import_module = import_module Unfiltered;
   process_module_binding = process_module_binding;
 }
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index e37299aad6..5e45957e83 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -97,11 +97,11 @@ val append_end_library_hook : (unit -> unit) -> unit
    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 : export:bool -> ModPath.t -> unit
+val import_module : Libobject.open_filter -> 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
+val import_modules : export:bool -> (Libobject.open_filter * ModPath.t) list -> unit
 
 (** Include  *)
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1f52641b82..08ba49f92b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -566,14 +566,21 @@ GRAMMAR EXTEND Gram
       | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
         ; qidl = LIST1 global ->
         { VernacRequire (Some ns, export, qidl) }
-      | IDENT "Import"; qidl = LIST1 global -> { VernacImport (false,qidl) }
-      | IDENT "Export"; qidl = LIST1 global -> { VernacImport (true,qidl) }
+      | IDENT "Import"; qidl = LIST1 filtered_import -> { VernacImport (false,qidl) }
+      | IDENT "Export"; qidl = LIST1 filtered_import -> { VernacImport (true,qidl) }
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
           { VernacInclude(e::l) }
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
          { warn_deprecated_include_type ~loc ();
         VernacInclude(e::l) } ] ]
   ;
+  filtered_import:
+    [ [ m = global -> { (m, ImportAll) }
+      | m = global; "("; ns = LIST1 one_import_filter_name SEP ","; ")" -> { (m, ImportNames ns) } ] ]
+  ;
+  one_import_filter_name:
+    [ [ n = global; etc = OPT [ "("; ".."; ")" -> { () } ] -> { n, Option.has_some etc } ] ]
+  ;
   export_token:
     [ [ IDENT "Import" -> { Some false }
       | IDENT "Export" -> { Some true }
diff --git a/vernac/library.ml b/vernac/library.ml
index 1b0bd4c0f7..01f5101764 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -335,7 +335,11 @@ let load_require _ (_,(needed,modl,_)) =
   List.iter register_library needed
 
 let open_require i (_,(_,modl,export)) =
-  Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export
+  Option.iter (fun export ->
+      let mpl = List.map (fun m -> Unfiltered, MPfile m) modl in
+      (* TODO support filters in Require *)
+      Declaremods.import_modules ~export mpl)
+    export
 
   (* [needed] is the ordered list of libraries not already loaded *)
 let cache_require o =
@@ -370,16 +374,17 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
   let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in
   let modrefl = List.map fst modrefl in
-    if Lib.is_module_or_modtype () then
-      begin
-        warn_require_in_module ();
-              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));
+  if Lib.is_module_or_modtype () then
+    begin
+      warn_require_in_module ();
+      add_anonymous_leaf (in_require (needed,modrefl,None));
+      Option.iter (fun export ->
+          (* TODO import filters *)
+          List.iter (fun m -> Declaremods.import_module Unfiltered ~export (MPfile m)) modrefl)
+        export
+    end
+  else
+    add_anonymous_leaf (in_require (needed,modrefl,export));
   ()
 
 (************************************************************************)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 475d5c31f7..3b9c771b93 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -877,9 +877,12 @@ let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
 let classify_syntax_definition (local, _ as o) =
   if local then Dispose else Substitute o
 
+let open_syntax_extension i o =
+  if Int.equal i 1 then cache_syntax_extension o
+
 let inSyntaxExtension : syntax_extension_obj -> obj =
   declare_object {(default_object "SYNTAX-EXTENSION") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o);
+       open_function = simple_open open_syntax_extension;
        cache_function = cache_syntax_extension;
        subst_function = subst_syntax_extension;
        classify_function = classify_syntax_definition}
@@ -1454,7 +1457,7 @@ let classify_notation nobj =
 
 let inNotation : notation_obj -> obj =
   declare_object {(default_object "NOTATION") with
-       open_function = open_notation;
+       open_function = simple_open open_notation;
        cache_function = cache_notation;
        subst_function = subst_notation;
        load_function = load_notation;
@@ -1765,7 +1768,7 @@ let classify_scope_command (local, _, _ as o) =
 let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
   declare_object {(default_object "DELIMITERS") with
       cache_function = cache_scope_command;
-      open_function = open_scope_command;
+      open_function = simple_open open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
       classify_function = classify_scope_command}
@@ -1831,7 +1834,7 @@ let classify_custom_entry (local,s as o) =
 let inCustomEntry : locality_flag * string -> obj =
   declare_object {(default_object "CUSTOM-ENTRIES") with
       cache_function = cache_custom_entry;
-      open_function = open_custom_entry;
+      open_function = simple_open open_custom_entry;
       load_function = load_custom_entry;
       subst_function = subst_custom_entry;
       classify_function = classify_custom_entry}
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 054b60853f..baaf8aa849 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -86,7 +86,13 @@ open Pputils
 
   let pr_module = Libnames.pr_qualid
 
-  let pr_import_module = Libnames.pr_qualid
+  let pr_one_import_filter_name (q,etc) =
+    Libnames.pr_qualid q ++ if etc then str "(..)" else mt()
+
+  let pr_import_module (m,f) =
+    Libnames.pr_qualid m ++ match f with
+    | ImportAll -> mt()
+    | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns)
 
   let sep_end = function
     | VernacBullet _
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3195f339b6..6de14997d4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -872,12 +872,62 @@ let vernac_constraint ~poly l =
 (**********************)
 (* Modules            *)
 
+let add_subnames_of ns full_n n =
+  let open GlobRef in
+  let module NSet = Globnames.ExtRefSet in
+  let add1 r ns = NSet.add (Globnames.TrueGlobal r) ns in
+  match n with
+  | Globnames.SynDef _ | Globnames.TrueGlobal (ConstRef _ | ConstructRef _ | VarRef _) ->
+    CErrors.user_err Pp.(str "Only inductive types can be used with Import (...).")
+  | Globnames.TrueGlobal (IndRef (mind,i)) ->
+    let open Declarations in
+    let dp = Libnames.dirpath full_n in
+    let mib = Global.lookup_mind mind in
+    let mip = mib.mind_packets.(i) in
+    let ns = add1 (IndRef (mind,i)) ns in
+    let ns = Array.fold_left_i (fun j ns _ -> add1 (ConstructRef ((mind,i),j+1)) ns)
+        ns mip.mind_consnames
+    in
+    List.fold_left (fun ns f ->
+        let s = Indrec.elimination_suffix f in
+        let n_elim = Id.of_string (Id.to_string mip.mind_typename ^ s) in
+        match Nametab.extended_global_of_path (Libnames.make_path dp n_elim) with
+        | exception Not_found -> ns
+        | n_elim -> NSet.add n_elim ns)
+      ns Sorts.all_families
+
+let interp_filter_in m = function
+  | ImportAll ->  Libobject.Unfiltered
+  | ImportNames ns ->
+    let module NSet = Globnames.ExtRefSet in
+    let dp_m = Nametab.dirpath_of_module m in
+    let ns =
+      List.fold_left (fun ns (n,etc) ->
+          let full_n =
+            let dp_n,n = repr_qualid n in
+            make_path (append_dirpath dp_m dp_n) n
+          in
+          let n = try Nametab.extended_global_of_path full_n
+            with Not_found ->
+              CErrors.user_err
+                Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++
+                    str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m))
+          in
+          let ns = NSet.add n ns in
+          if etc then add_subnames_of ns full_n n else ns)
+        NSet.empty ns
+    in
+    Libobject.Names ns
+
 let vernac_import 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
+  let import_mod (qid,f) =
+    let m = try Nametab.locate_module qid
+      with Not_found ->
+        CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
+    in
+    let f = interp_filter_in m f in
+    Declaremods.import_module f ~export m
+  in
   List.iter import_mod refl
 
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
@@ -893,7 +943,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
-  Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export
 
 let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -914,7 +964,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [qualid_of_ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export
          ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -929,14 +979,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
          (str "Module " ++ Id.print id ++ str " is defined");
-       Option.iter (fun export -> vernac_import export [qualid_of_ident id])
+       Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll])
          export
 
 let vernac_end_module export {loc;v=id} =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
-  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export
 
 let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Global.sections_are_opened () then
@@ -957,7 +1007,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
+             (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export
          ) argsexport
 
     | _ :: _ ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d6e7a3947a..27663a0681 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -101,7 +101,14 @@ type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
+
 type export_flag    = bool (* true = Export;        false = Import         *)
+
+type one_import_filter_name = qualid * bool (* import inductive components *)
+type import_filter_expr =
+  | ImportAll
+  | ImportNames of one_import_filter_name list
+
 type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
@@ -320,7 +327,7 @@ type nonrec vernac_expr =
   | VernacEndSegment of lident
   | VernacRequire of
       qualid option * export_flag option * qualid list
-  | VernacImport of export_flag * qualid list
+  | VernacImport of export_flag * (qualid * import_filter_expr) list
   | VernacCanonical of qualid or_by_notation
   | VernacCoercion of qualid or_by_notation *
       class_rawexpr * class_rawexpr