tjh.dev
1diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
2index a9c5074..eed92e3 100644
3--- a/serapi/serapi_paths.ml
4+++ b/serapi/serapi_paths.ml
5@@ -23,10 +23,10 @@
6 let coq_loadpath_default ~implicit ~coq_path =
7 let open Loadpath in
8 let mk_path prefix = coq_path ^ "/" ^ prefix in
9- let mk_lp ~ml ~root ~dir ~implicit =
10+ let mk_lp ~ml ~root ~dir ~implicit ~absolute =
11 { recursive = true;
12 path_spec = VoPath {
13- unix_path = mk_path dir;
14+ unix_path = if absolute then dir else mk_path dir;
15 coq_path = root;
16 has_ml = ml;
17 implicit;
18@@ -35,11 +35,11 @@ let coq_loadpath_default ~implicit ~coq_path =
19 (* in 8.8 we can use Libnames.default_* *)
20 let coq_root = Names.DirPath.make [Libnames.coq_root] in
21 let default_root = Libnames.default_root_prefix in
22- [mk_lp ~ml:AddRecML ~root:coq_root ~implicit ~dir:"plugins";
23- mk_lp ~ml:AddNoML ~root:coq_root ~implicit ~dir:"theories";
24- mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
25+ [mk_lp ~ml:AddRecML ~root:coq_root ~implicit ~dir:"plugins" ~absolute:false;
26+ mk_lp ~ml:AddNoML ~root:coq_root ~implicit ~dir:"theories" ~absolute:false;
27+ mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
28 ] @
29- List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir)
30+ List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir ~absolute:true)
31 Envars.coqpath
32
33 (******************************************************************************)