diff options
| author | Emilio Jesus Gallego Arias | 2020-10-19 14:19:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-10-21 20:16:36 +0200 |
| commit | 0730062742daab12000d950b8f34f05fd72ca5cd (patch) | |
| tree | 99a8beb213a245d5e7b1077c606d4769000370ef /toplevel | |
| parent | f8a0b47dee445bb71e0824df576f69dd56511257 (diff) | |
[coqinit] Cosmetics on long list append.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 68db320b9d..501047c520 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -89,21 +89,23 @@ let libs_init_load_path ~coqlib = let misc_ml, misc_vo = List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in - plugins_dirs @ contrib_ml @ List.concat misc_ml, - - (* current directory (not recursively!) *) - [ { unix_path = "." - ; coq_path = Libnames.default_root_prefix - ; implicit = false - ; has_ml = true - ; recursive = false - } ] @ + let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in + let vo_loadpath = + (* current directory (not recursively!) *) + [ { unix_path = "." + ; coq_path = Libnames.default_root_prefix + ; implicit = false + ; has_ml = true + ; recursive = false + } ] @ - (* then standard library *) - [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ + (* then standard library *) + [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ - (* then user-contrib *) - contrib_vo @ + (* then user-contrib *) + contrib_vo @ - (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.concat misc_vo + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) + List.concat misc_vo + in + ml_loadpath, vo_loadpath |