Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fix for Rocq/Rational.)"

This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69.

Conflicts:
	CHANGES

2 files changed, 5 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 7cd2c2499..8adda6039 100644
--- a/CHANGES
+++ b/CHANGES
@@ -99,8 +99,11 @@ Tools
   the load path and the ml path, use -I -as.
 - Option -Q behaves as -I -as and -R, except that the logical path of
   any loaded file has to be fully qualified.
-- Option -nois loads coq/theories and coq/plugins as if using -Q rather
-  than -R. (Same behavior as with coq/user-contrib.)
+- Option -R no longer adds recursively to the ml path; only the root
+  directory is added. (Behavior with respect to the load path is
+  unchanged.)
+- Option -nois prevents coq/theories and coq/plugins to be recursively
+  added to the load path. (Same behavior as with coq/user-contrib.)
 
 Internal Infrastructure
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 458fe8ef0..196ab98ed 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -180,7 +180,6 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in
     let () = add_ml_dir unix_path in
     let add (path, dir) =
       Loadpath.add_load_path path Loadpath.ImplicitPath dir in