aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 80c81d243..e7f56ef87 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -80,16 +80,19 @@ let init_load_path () =
List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
add_ml_include camlp4;
- Mltop.add_path "." [Nametab.default_root];
+ Mltop.add_path "." Nametab.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
List.iter
(fun (s,alias,reci) ->
if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
(List.rev !includes)
+(* Must be done after restoring initial state! *)
let init_library_roots () =
List.iter
- (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes;
+ (fun (_,alias,_) ->
+ if alias <> [] then Nametab.push_library_root (List.hd alias))
+ !includes;
includes := []
(* Initialises the Ocaml toplevel before launching it, so that it can