From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 22:12:02 +0200 Subject: [flags] Remove XML output flag. This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. --- library/declaremods.mli | 8 -------- 1 file changed, 8 deletions(-) (limited to 'library/declaremods.mli') 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 -- cgit v1.2.3