From 1ea09cb57dffd7cc9b6fa3ccec137ea3dfcc6980 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 24 Sep 2016 23:33:10 +0200 Subject: The coqtop options -Q and -R do not affect the ML loadpath anymore. It seems that such options were adding the considered path to the ML loadpath as well, which is not what is documented, and does not provide an atomic way to manipulate Coq loadpaths. --- toplevel/coqinit.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- cgit v1.2.3