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