diff options
author | 2004-03-30 16:09:42 +0000 | |
---|---|---|
committer | 2004-03-30 16:09:42 +0000 | |
commit | 45ed02f40b41c5e064d68a4bb364fd4bbe5cba07 (patch) | |
tree | 47c646117a35ddd91941d5b11b7e86b1643ab70b /library/library.ml | |
parent | 1fd9493d186f82e908412fbc3568f1f2358d8606 (diff) |
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
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/library.ml b/library/library.ml index 82c1b600d..c17db9afb 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 () |