The XML exportation hook for require is now active for:

 - Require id.
 - Require Export id.
 - Require "file".
 - Require Export "file".


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5618 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 0 deletions

diff --git a/library/library.ml b/library/library.ml
index 82c1b600dd..c17db9afb1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -585,6 +585,7 @@ let require_library_from_file spec idopt file export =
     end
     else
       add_anonymous_leaf (in_require ([modref],Some export));
+    if !Options.xml_export then !xml_require modref;
     add_frozen_state ()
 
 
@@ -593,12 +594,14 @@ let require_library_from_file spec idopt file export =
 let read_library qid =
   let modref = rec_intern_qualified_library qid in
   add_anonymous_leaf (in_require ([modref],None));
+  if !Options.xml_export then !xml_require modref;
   add_frozen_state ()
 
 let read_library_from_file f =
   let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
   let modref = rec_intern_by_filename_only None f in
   add_anonymous_leaf (in_require ([modref],None));
+  if !Options.xml_export then !xml_require modref;
   add_frozen_state ()