diff options
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 6a99aedc8..a6a8937ba 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -401,7 +401,7 @@ let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); try (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in - read_library (dummy_loc,qid); + require_library [dummy_loc,qid] None; msg (str "opening... "); Declaremods.import_module false (Nametab.locate_module qid); msgnl (str "done" ++ fnl ()); |