aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqinit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8a8dbe9601..acbf909cc6 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -108,7 +108,7 @@ let init_load_path () =
(* additional loadpath, given with options -Q and -R *)
List.iter
(fun (unix_path, coq_root, implicit) ->
- Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
+ Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
(List.rev !includes);
(* additional ml directories, given with option -I *)
List.iter Mltop.add_ml_dir (List.rev !ml_includes)