aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 32ac9a496d..b7f1e4a197 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -171,8 +171,8 @@ let load_vernacular () =
let load_vernacular_obj = ref ([] : string list)
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
let load_vernac_obj () =
- List.iter (fun f -> Library.require_library_from_file f None)
- (List.rev !load_vernacular_obj)
+ let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+ Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
let require_prelude () =
let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in