correctly open objects for Names filters

1 files changed, 4 insertions, 2 deletions

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;