Merge PR #773: [flags] Remove XML output flag.

1 files changed, 0 insertions, 3 deletions

diff --git a/library/library.ml b/library/library.ml
index 20ecc2c229..28afa054e9 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -551,8 +551,6 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
-
 let warn_require_in_module =
   CWarnings.create ~name:"require-in-module" ~category:"deprecated"
                    (fun () -> strbrk "Require inside a module is" ++
@@ -574,7 +572,6 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
   ()
 
 (* the function called by Vernacentries.vernac_import *)