From 45ed02f40b41c5e064d68a4bb364fd4bbe5cba07 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 30 Mar 2004 16:09:42 +0000
Subject: 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
---
 library/library.ml | 3 +++
 1 file changed, 3 insertions(+)

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 ()
 
 
-- 
cgit v1.2.3