Merge PR #11820: Partial imports

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

43 files changed, 465 insertions, 140 deletions

diff --git a/checker/check.ml b/checker/check.ml
index bb3255338f..4212aac6ea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -305,7 +305,7 @@ let marshal_in_segment ~validate ~value f ch =
       with _ ->
         user_err (str "Corrupted file " ++ quote (str f))
     in
-    let () = Validate.validate ~debug:!Flags.debug value v in
+    let () = Validate.validate value v in
     let v = Analyze.instantiate v in
     Obj.obj v, stop, digest
   else
diff --git a/checker/validate.ml b/checker/validate.ml
index 66367cb002..20884c4d01 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -208,11 +208,10 @@ let print_frame = function
 | CtxField i -> Printf.sprintf "fld=%i" i
 | CtxTag i -> Printf.sprintf "tag=%i" i
 
-let validate ~debug v (o, mem) =
+let validate v (o, mem) =
   try val_gen v mem mt_ec o
   with ValidObjError(msg,ctx,obj) ->
-    (if debug then
-      let ctx = List.rev_map print_frame ctx in
-      print_endline ("Context: "^String.concat"/"ctx);
-      pr_obj mem obj);
+    let rctx = List.rev_map print_frame ctx in
+    print_endline ("Context: "^String.concat"/"rctx);
+    pr_obj mem obj;
     failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
diff --git a/checker/validate.mli b/checker/validate.mli
index 9ddc510e4a..1204b528f9 100644
--- a/checker/validate.mli
+++ b/checker/validate.mli
@@ -10,4 +10,4 @@
 
 open Analyze
 
-val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit
+val validate : Values.value -> data * obj LargeArray.t -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 12f7135cdf..b9efce6948 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -372,6 +372,17 @@ let v_compiled_lib =
 
 let v_obj = Dyn
 
+let v_globref = Sum("globref",0,[|
+    [|v_id|];
+    [|v_cst|];
+    [|v_ind|];
+    [|v_cons|]
+  |])
+
+let v_ext_gref = Sum("extended_global_reference",0,[|[|v_globref|];[|v_kn|]|])
+
+let v_open_filter = Sum ("open_filter",1,[|[|v_hset v_ext_gref|]|])
+
 let rec v_aobjs = Sum("algebraic_objects", 0,
   [| [|v_libobjs|];
      [|v_mp;v_subst|]
@@ -383,7 +394,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| List v_mp |];
+     [| List (v_pair v_open_filter v_mp)|];
      [| v_obj |]
   |])
 
diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
new file mode 100644
index 0000000000..4170799be7
--- /dev/null
+++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then
+
+    elpi_CI_REF=partial-import
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78b1f02383..57c8683aaa 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -422,7 +422,12 @@ are now available through the dot notation.
    If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of
    :token:`module_binder`\s.
 
-.. cmd:: Import {+ @qualid }
+.. cmd:: Import {+ @filtered_import }
+
+   .. insertprodn filtered_import filtered_import
+
+   .. prodn::
+      filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) }
 
    If :token:`qualid` denotes a valid basic module (i.e. its module type is a
    signature), makes its components available by their short names.
@@ -465,12 +470,50 @@ are now available through the dot notation.
 
          Check B.T.
 
-.. cmd:: Export {+ @qualid }
+   Appending a module name with a parenthesized list of names will
+   make only those names available with short names, not other names
+   defined in the module nor will it activate other features.
+
+   The names to import may be constants, inductive types and
+   constructors, and notation aliases (for instance, Ltac definitions
+   cannot be selectively imported). If they are from an inner module
+   to the one being imported, they must be prefixed by the inner path.
+
+   The name of an inductive type may also be followed by ``(..)`` to
+   import it, its constructors and its eliminators if they exist. For
+   this purpose "eliminator" means a constant in the same module whose
+   name is the inductive type's name suffixed by one of ``_sind``,
+   ``_ind``, ``_rec`` or ``_rect``.
+
+   .. example::
+
+      .. coqtop:: reset in
+
+         Module A.
+         Module B.
+         Inductive T := C.
+         Definition U := nat.
+         End B.
+         Definition Z := Prop.
+         End A.
+         Import A(B.T(..), Z).
+
+      .. coqtop:: all
+
+         Check B.T.
+         Check B.C.
+         Check Z.
+         Fail Check B.U.
+         Check A.B.U.
+
+.. cmd:: Export {+ @filtered_import }
    :name: Export
 
    Similar to :cmd:`Import`, except that when the module containing this command
    is imported, the :n:`{+ @qualid }` are imported as well.
 
+   The selective import syntax also works with Export.
+
    .. exn:: @qualid is not a module.
       :undocumented:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a01f57eb22..5034d9a3c9 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -511,6 +511,12 @@ strategy_flag: [
 | OPTINREF
 ]
 
+filtered_import: [
+| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")"
+| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ]
+| DELETE global
+]
+
 functor_app_annot: [
 | OPTINREF
 ]
@@ -1582,6 +1588,7 @@ SPLICE: [
 | searchabout_queries
 | locatable
 | scope_delimiter
+| one_import_filter_name
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index dc7e0fba37..04c20a7203 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1031,8 +1031,8 @@ gallina_ext: [
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
 | "From" global "Require" export_token LIST1 global
-| "Import" LIST1 global
-| "Export" LIST1 global
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ext_module_expr
 | "Include" "Type" module_type_inl LIST0 ext_module_type
 | "Transparent" LIST1 smart_global
@@ -1057,6 +1057,15 @@ gallina_ext: [
 | "Export" "Unset" option_table
 ]
 
+filtered_import: [
+| global
+| global "(" LIST1 one_import_filter_name SEP "," ")"
+]
+
+one_import_filter_name: [
+| global OPT [ "(" ".." ")" ]
+]
+
 export_token: [
 | "Import"
 | "Export"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index ac986f9adf..e71c80f829 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -497,6 +497,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+filtered_import: [
+| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
+]
+
 cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
@@ -849,8 +853,8 @@ command: [
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "Import" LIST1 qualid
-| "Export" LIST1 qualid
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
 | "Transparent" LIST1 smart_qualid
diff --git a/interp/notation.ml b/interp/notation.ml
index 6291a88bb0..0afbb9cd62 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) =
 let inScope : bool * bool * scope_item -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
-      open_function = open_scope;
+      open_function = simple_open open_scope;
       subst_function = subst_scope;
       discharge_function = discharge_scope;
       classify_function = classify_scope }
@@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) =
 let classify_prim_token_interpretation infos =
     if infos.pt_local then Dispose else Substitute infos
 
+let open_prim_token_interpretation i o =
+  if Int.equal i 1 then cache_prim_token_interpretation o
+
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
-     open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+     open_function  = simple_open open_prim_token_interpretation;
      cache_function = cache_prim_token_interpretation;
      subst_function = subst_prim_token_interpretation;
      classify_function = classify_prim_token_interpretation}
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 767c69e3b6..7184f5ea29 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -67,11 +67,18 @@ let subst_syntax_constant (subst,(local,syndef)) =
 let classify_syntax_constant (local,_ as o) =
   if local then Dispose else Substitute o
 
+let filtered_open_syntax_constant f i ((_,kn),_ as o) =
+  let in_f = match f with
+    | Unfiltered -> true
+    | Names ns -> Globnames.(ExtRefSet.mem (SynDef kn) ns)
+  in
+  if in_f then open_syntax_constant i o
+
 let in_syntax_constant : (bool * syndef) -> obj =
   declare_object {(default_object "SYNDEF") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
-    open_function = open_syntax_constant;
+    open_function = filtered_open_syntax_constant;
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
 
 type family = InSProp | InProp | InSet | InType
 
+let all_families = [InSProp; InProp; InSet; InType]
+
 type t =
   | SProp
   | Prop
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
 
 type family = InSProp | InProp | InSet | InType
 
+val all_families : family list
+
 type t = private
   | SProp
   | Prop
diff --git a/library/globnames.ml b/library/globnames.ml
index 9126a467bf..bc24fbf096 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -117,3 +117,10 @@ module ExtRefOrdered = struct
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
+
+module ExtRefMap = HMap.Make(ExtRefOrdered)
+module ExtRefSet = ExtRefMap.Set
+
+let subst_extended_reference sub = function
+  | SynDef kn -> SynDef (subst_kn sub kn)
+  | TrueGlobal gr -> TrueGlobal (subst_global_reference sub gr)
diff --git a/library/globnames.mli b/library/globnames.mli
index fb1583e16c..8acea5ef28 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -61,3 +61,10 @@ module ExtRefOrdered : sig
   val equal : t -> t -> bool
   val hash : t -> int
 end
+
+module ExtRefSet : CSig.SetS with type elt = extended_global_reference
+module ExtRefMap : CMap.ExtS
+  with type key = extended_global_reference
+   and module Set := ExtRefSet
+
+val subst_extended_reference : substitution -> extended_global_reference -> extended_global_reference
diff --git a/library/goptions.ml b/library/goptions.ml
index 73132868d7..1418407533 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -90,7 +90,7 @@ module MakeTable =
         let inGo : option_mark * A.t -> obj =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
-                Libobject.open_function = load_options;
+                Libobject.open_function = simple_open load_options;
                 Libobject.cache_function = cache_options;
                 Libobject.subst_function = subst_options;
                 Libobject.classify_function = (fun x -> Substitute x)}
@@ -262,7 +262,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
         declare_object
           { (default_object (nickname key)) with
             load_function = load_options;
-            open_function = open_options;
+            open_function = simple_open open_options;
             cache_function = cache_options;
             subst_function = subst_options;
             discharge_function = discharge_options;
diff --git a/library/lib.ml b/library/lib.ml
index e7e6dc640a..830777003b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -46,7 +46,7 @@ let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
 
 let load_atomic_objects i pr = iter_objects load_object i pr
-let open_atomic_objects i pr = iter_objects open_object i pr
+let open_atomic_objects f i pr = iter_objects (open_object f) i pr
 
 let subst_atomic_objects subst seg =
   let subst_one = fun (id,obj as node) ->
diff --git a/library/lib.mli b/library/lib.mli
index 949b5e26c2..56ea35ec60 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -35,7 +35,8 @@ type lib_objects = (Id.t * Libobject.t) list
 
 (** {6 Object iteration functions. } *)
 
-val open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
+val open_atomic_objects : Libobject.open_filter
+  -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit
 val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
 val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_objects
 (*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
diff --git a/library/libobject.ml b/library/libobject.ml
index 0681e12449..c38e0d891b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -18,11 +18,36 @@ type 'a substitutivity =
 
 type object_name = Libnames.full_path * Names.KerName.t
 
+module NSet = Globnames.ExtRefSet
+
+type open_filter =
+  | Unfiltered
+  | Names of NSet.t
+
+let simple_open f filter i o = match filter with
+  | Unfiltered -> f i o
+  | Names _ -> ()
+
+let filter_and f1 f2 = match f1, f2 with
+  | Unfiltered, f | f, Unfiltered -> Some f
+  | Names n1, Names n2 ->
+    let n = NSet.inter n1 n2 in
+    if NSet.is_empty n then None
+    else Some (Names n)
+
+let filter_or f1 f2 = match f1, f2 with
+  | Unfiltered, f | f, Unfiltered -> Unfiltered
+  | Names n1, Names n2 -> Names (NSet.union n1 n2)
+
+let in_filter_ref gr = function
+  | Unfiltered -> true
+  | Names ns -> NSet.mem (Globnames.TrueGlobal gr) ns
+
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
-  open_function : int -> object_name * 'a -> unit;
+  open_function : open_filter -> int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
   subst_function : Mod_subst.substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
@@ -32,7 +57,7 @@ let default_object s = {
   object_name = s;
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
-  open_function = (fun _ _ -> ());
+  open_function = (fun _ _ _ -> ());
   subst_function = (fun _ ->
     CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
   classify_function = (fun atomic_obj -> Keep atomic_obj);
@@ -75,7 +100,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ExportObject of { mpl : ModPath.t list }
+  | ExportObject of { mpl : (open_filter * ModPath.t) list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
@@ -105,9 +130,9 @@ let load_object i (sp, Dyn.Dyn (tag, v)) =
   let decl = DynMap.find tag !cache_tab in
   decl.load_function i (sp, v)
 
-let open_object i (sp, Dyn.Dyn (tag, v)) =
+let open_object f i (sp, Dyn.Dyn (tag, v)) =
   let decl = DynMap.find tag !cache_tab in
-  decl.open_function i (sp, v)
+  decl.open_function f i (sp, v)
 
 let subst_object (subs, Dyn.Dyn (tag, v)) =
   let decl = DynMap.find tag !cache_tab in
@@ -147,7 +172,7 @@ let global_object_nodischarge s ~cache ~subst =
   let import i o = if Int.equal i 1 then cache o in
   { (default_object s) with
     cache_function = cache;
-    open_function = import;
+    open_function = simple_open import;
     subst_function = (match subst with
         | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
         | Some subst -> subst;
diff --git a/library/libobject.mli b/library/libobject.mli
index 24cadc2223..1c82349bb6 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -72,16 +72,28 @@ type 'a substitutivity =
 
 type object_name = full_path * Names.KerName.t
 
+type open_filter = Unfiltered | Names of Globnames.ExtRefSet.t
+
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
-  open_function : int -> object_name * 'a -> unit;
+  open_function : open_filter -> int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
   subst_function :  substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
+val simple_open : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+(** Combinator for making objects which are only opened by unfiltered Import *)
+
+val filter_and : open_filter -> open_filter -> open_filter option
+(** Returns [None] when the intersection is empty. *)
+
+val filter_or :  open_filter -> open_filter -> open_filter
+
+val in_filter_ref : Names.GlobRef.t -> open_filter -> bool
+
 (** The default object is a "Keep" object with empty methods.
    Object creators are advised to use the construction
    [{(default_object "MY_OBJECT") with
@@ -114,7 +126,7 @@ and t =
   | ModuleTypeObject of substitutive_objects
   | IncludeObject of algebraic_objects
   | KeepObject of objects
-  | ExportObject of { mpl : Names.ModPath.t list }
+  | ExportObject of { mpl : (open_filter * Names.ModPath.t) list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
@@ -129,7 +141,7 @@ val declare_object :
 
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
-val open_object : int -> object_name * obj -> unit
+val open_object : open_filter -> int -> object_name * obj -> unit
 val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
diff --git a/library/nametab.ml b/library/nametab.ml
index 523fe8af50..d9b4dc9122 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -352,10 +352,8 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = HMap.Make(ExtRefOrdered)
-
-type globrevtab = full_path Globrevtab.t
-let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
+type globrevtab = full_path ExtRefMap.t
+let the_globrevtab = Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
 
 
 type mprevtab = DirPath.t MPmap.t
@@ -386,7 +384,7 @@ let push_xref visibility sp xref =
   match visibility with
     | Until _ ->
         the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-        the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+        the_globrevtab := ExtRefMap.add xref sp !the_globrevtab
     | _ ->
         begin
           if ExtRefTab.exists sp !the_ccitab then
@@ -520,7 +518,7 @@ let path_of_global ref =
   let open GlobRef in
   match ref with
     | VarRef id -> make_path DirPath.empty id
-    | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
+    | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
   fst (repr_path (path_of_global ref))
@@ -529,7 +527,7 @@ let basename_of_global ref =
   snd (repr_path (path_of_global ref))
 
 let path_of_syndef kn =
-  Globrevtab.find (SynDef kn) !the_globrevtab
+  ExtRefMap.find (SynDef kn) !the_globrevtab
 
 let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
@@ -547,7 +545,7 @@ let shortest_qualid_of_global ?loc ctx ref =
   match ref with
     | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
-        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+        let sp = ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
         ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef ?loc ctx kn =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4127d28bae..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
 
 let inTacticGrammar : tactic_grammar_obj -> obj =
   declare_object {(default_object "TacticGrammar") with
-       open_function = open_tactic_notation;
+       open_function = simple_open open_tactic_notation;
        load_function = load_tactic_notation;
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
-     open_function   = open_md;
+     open_function   = simple_open open_md;
      subst_function = subst_md;
      classify_function = classify_md}
 
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index 4f00f17892..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -32,7 +32,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
       { (default_object name) with
         cache_function = cache;
         load_function = (fun _ -> load);
-        open_function = (fun _ -> load);
+        open_function = simple_open (fun _ -> load);
         classify_function = (fun (local, tac) ->
           if local then Dispose else Substitute (local, tac));
         subst_function = subst}
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 324007930a..5135d72f7b 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -93,13 +93,14 @@ let load_constant i ((sp,kn), obj) =
   Dumpglob.add_constant_kind con obj.cst_kind
 
 (* Opening means making the name without its module qualification available *)
-let open_constant i ((sp,kn), obj) =
+let open_constant f i ((sp,kn), obj) =
   (* Never open a local definition *)
   match obj.cst_locl with
   | ImportNeedQualified -> ()
   | ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
-    Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
+    if in_filter_ref (GlobRef.ConstRef con) f then
+      Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
 
 let exists_name id =
   Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f8a46fcb1d..2118b4f231 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1163,7 +1163,7 @@ let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
                     load_function = load_autohint;
-                    open_function = open_autohint;
+                    open_function = simple_open open_autohint;
                     subst_function = subst_autohint;
                     classify_function = classify_autohint; }
 
diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out
new file mode 100644
index 0000000000..ce484889b3
--- /dev/null
+++ b/test-suite/output/UselessSyndef.out
@@ -0,0 +1,2 @@
+a
+     : nat
diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v
new file mode 100644
index 0000000000..96ad6e9f5c
--- /dev/null
+++ b/test-suite/output/UselessSyndef.v
@@ -0,0 +1,10 @@
+Module M.
+  Definition a := 0.
+End M.
+Module N.
+  Notation a := M.a (only parsing).
+End N.
+
+Import M. Import N.
+
+Check a.
diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v
new file mode 100644
index 0000000000..720083aec5
--- /dev/null
+++ b/test-suite/success/PartialImport.v
@@ -0,0 +1,58 @@
+Module M.
+
+  Definition a := 0.
+  Definition b := 1.
+
+  Module N.
+
+    Notation c := (a + b).
+
+  End N.
+
+  Inductive even : nat -> Prop :=
+  | even_0 : even 0
+  | even_S n : odd n -> even (S n)
+  with odd : nat -> Set :=
+    odd_S n : even n -> odd (S n).
+
+End M.
+
+Module Simple.
+
+  Import M(a).
+
+  Check a.
+  Fail Check b.
+  Fail Check N.c.
+
+  (* todo output test: this prints a+M.b since the notation isn't imported *)
+  Check M.N.c.
+
+  Fail Import M(c).
+  Fail Import M(M.b).
+
+  Import M(N.c).
+  Check N.c.
+  (* interestingly prints N.c (also does with unfiltered Import M) *)
+
+  Import M(even(..)).
+  Check even. Check even_0. Check even_S.
+  Check even_sind. Check even_ind.
+  Fail Check even_rect. (* doesn't exist *)
+  Fail Check odd. Check M.odd.
+  Fail Check odd_S. Fail Check odd_sind.
+
+End Simple.
+
+Module WithExport.
+
+  Module X.
+    Export M(a, N.c).
+  End X.
+
+  Import X.
+  Check a.
+  Check N.c. (* also prints N.c *)
+  Fail Check b.
+
+End WithExport.
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index ebc63ddd01..3e920fcc2d 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -91,7 +91,7 @@ let inTacDef : tacdef -> obj =
   declare_object {(default_object "TAC2-DEFINITION") with
      cache_function  = cache_tacdef;
      load_function   = load_tacdef;
-     open_function   = open_tacdef;
+     open_function   = simple_open open_tacdef;
      subst_function = subst_tacdef;
      classify_function = classify_tacdef}
 
@@ -198,7 +198,7 @@ let inTypDef : typdef -> obj =
   declare_object {(default_object "TAC2-TYPE-DEFINITION") with
      cache_function  = cache_typdef;
      load_function   = load_typdef;
-     open_function   = open_typdef;
+     open_function   = simple_open open_typdef;
      subst_function = subst_typdef;
      classify_function = classify_typdef}
 
@@ -268,7 +268,7 @@ let inTypExt : typext -> obj =
   declare_object {(default_object "TAC2-TYPE-EXTENSION") with
      cache_function  = cache_typext;
      load_function   = load_typext;
-     open_function   = open_typext;
+     open_function   = simple_open open_typext;
      subst_function = subst_typext;
      classify_function = classify_typext}
 
@@ -664,7 +664,7 @@ let classify_synext o =
 let inTac2Notation : synext -> obj =
   declare_object {(default_object "TAC2-NOTATION") with
      cache_function  = cache_synext;
-     open_function   = open_synext;
+     open_function   = simple_open open_synext;
      subst_function = subst_synext;
      classify_function = classify_synext}
 
@@ -694,7 +694,7 @@ let inTac2Abbreviation : abbreviation -> obj =
   declare_object {(default_object "TAC2-ABBREVIATION") with
      cache_function  = cache_abbreviation;
      load_function   = load_abbreviation;
-     open_function   = open_abbreviation;
+     open_function   = simple_open open_abbreviation;
      subst_function = subst_abbreviation;
      classify_function = classify_abbreviation}
 
@@ -747,7 +747,7 @@ let classify_redefinition o = Substitute o
 let inTac2Redefinition : redefinition -> obj =
   declare_object {(default_object "TAC2-REDEFINITION") with
      cache_function  = perform_redefinition;
-     open_function   = (fun _ -> perform_redefinition);
+     open_function   = simple_open (fun _ -> perform_redefinition);
      subst_function = subst_redefinition;
      classify_function = classify_redefinition }
 
@@ -962,7 +962,7 @@ let inTac2Init : unit -> obj =
   declare_object {(default_object "TAC2-INIT") with
     cache_function = cache_ltac2_init;
     load_function = load_ltac2_init;
-    open_function = open_ltac2_init;
+    open_function = simple_open open_ltac2_init;
   }
 
 let _ = Mltop.declare_cache_obj begin fun () ->
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