diff options
| author | Emilio Jesus Gallego Arias | 2020-02-13 21:14:01 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 21:14:01 +0100 |
| commit | 83052eff43d3eeff96462286b69249ef868bf5f0 (patch) | |
| tree | bd2b80422e44573f89a79d518184e6b0b5405891 /toplevel | |
| parent | 9193769161e1f06b371eed99dfe9e90fec9a14a6 (diff) | |
[coqinit] Removed unused `with_ml` parameter.
`theories` now never have `.ml` files inside.
Diffstat (limited to 'toplevel')
| -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 |