diff options
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 005594b8d..9d750b616 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -63,14 +63,6 @@ val start_modtype : val end_modtype : unit -> module_path -(** Hooks for XML output *) -val xml_declare_module : (module_path -> unit) Hook.t -val xml_start_module : (module_path -> unit) Hook.t -val xml_end_module : (module_path -> unit) Hook.t -val xml_declare_module_type : (module_path -> unit) Hook.t -val xml_start_module_type : (module_path -> unit) Hook.t -val xml_end_module_type : (module_path -> unit) Hook.t - (** {6 Libraries i.e. modules on disk } *) type library_name = DirPath.t |