aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e95f59f67..0e52fe6ab 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -93,9 +93,10 @@ let init_load_path () =
(* first, developer specific directory to open *)
if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
(* main loops *)
- if Coq_config.local || !Flags.boot then
+ if Coq_config.local || !Flags.boot then begin
let () = Mltop.add_ml_dir (coqlib/"stm") in
- Mltop.add_ml_dir (coqlib/"ide");
+ Mltop.add_ml_dir (coqlib/"ide")
+ end;
Mltop.add_ml_dir (coqlib/"toploop");
(* then standard library *)
add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;