diff options
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |