diff options
| -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 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 () |