diff options
| author | Gaëtan Gilbert | 2020-02-24 14:24:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | b98ef72ee300e52dd2c67f03da358e3c2102cdbb (patch) | |
| tree | ceddc2c4523978cfa0436047b44f3f326eeba106 /vernac/declaremods.mli | |
| parent | 2d6b7d5997037d9a94524a733867f64cd34e851c (diff) | |
pass filters around
Diffstat (limited to 'vernac/declaremods.mli')
| -rw-r--r-- | vernac/declaremods.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |