correctly open objects for Names filters

6 files changed, 23 insertions, 11 deletions

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d6aa527f4d..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 = todo_filter open_syntax_constant;
+    open_function = filtered_open_syntax_constant;
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 392a64e5d0..c38e0d891b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,8 +28,6 @@ let simple_open f filter i o = match filter with
   | Unfiltered -> f i o
   | Names _ -> ()
 
-let todo_filter = simple_open
-
 let filter_and f1 f2 = match f1, f2 with
   | Unfiltered, f | f, Unfiltered -> Some f
   | Names n1, Names n2 ->
@@ -41,6 +39,10 @@ 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;
diff --git a/library/libobject.mli b/library/libobject.mli
index 27b47264a6..1c82349bb6 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -92,7 +92,7 @@ val filter_and : open_filter -> open_filter -> open_filter option
 
 val filter_or :  open_filter -> open_filter -> open_filter
 
-val todo_filter : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+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
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 38f6db2db3..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)
@@ -135,7 +136,7 @@ let (objConstant : constant_obj Libobject.Dyn.tag) =
   declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
-    open_function = todo_filter open_constant;
+    open_function = open_constant;
     classify_function = classify_constant;
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 203e11d6ab..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
@@ -65,7 +68,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag =
   declare_object_full {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
-    open_function = todo_filter open_inductive;
+    open_function = open_inductive;
     classify_function = (fun a -> Substitute a);
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive;
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index b87d3c5681..438509e28a 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -388,7 +388,6 @@ and open_include f i ((sp,kn), aobjs) =
   open_objects f i prefix o
 
 and open_export f i mpl =
-  let _ = todo_filter in (* exports will have their own filters! *)
   let _,objs = collect_export f i mpl (MPmap.empty, []) in
   List.iter (fun (f,o) -> open_object f 1 o) objs