diff options
| -rw-r--r-- | toplevel/coqinit.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index b353f8aff1..3aa9acfc52 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -51,12 +51,11 @@ let load_rcfile ~rcfile ~state = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise -(* Recursively puts dir in the LoadPath if -nois was not passed *) -let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = +(* Recursively puts `.v` files in the LoadPath if -nois was not passed *) +let build_stdlib_vo_path ~load_init ~unix_path ~coq_path = let open Loadpath in - let add_ml = if with_ml then AddRecML else AddNoML in { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } + path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = load_init } } let build_stdlib_ml_path ~dir = @@ -108,7 +107,7 @@ let libs_init_load_path ~load_init = (* then standard library *) [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ - [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false] @ + [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) (if Sys.file_exists user_contrib then |