1 files changed, 23 insertions, 12 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 9faa455657..68db320b9d 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -56,14 +56,21 @@ let build_stdlib_vo_path ~unix_path ~coq_path =
   let open Loadpath in
   { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
 
+(* Note we don't use has_ml=true due to #12771 , we need to see if we
+   should just remove that option *)
 let build_userlib_path ~unix_path =
   let open Loadpath in
-  { unix_path
-  ; coq_path = Libnames.default_root_prefix
-  ; has_ml = true
-  ; implicit = false
-  ; recursive = true
-  }
+  if Sys.file_exists unix_path then
+    let ml_path = System.all_subdirs ~unix_path |> List.map fst in
+    let vo_path =
+      { unix_path
+      ; coq_path = Libnames.default_root_prefix
+      ; has_ml = false
+      ; implicit = false
+      ; recursive = true
+      } in
+    ml_path, [vo_path]
+  else [], []
 
 (* LoadPath for Coq user libraries *)
 let libs_init_load_path ~coqlib =
@@ -75,8 +82,14 @@ let libs_init_load_path ~coqlib =
   let coq_path = Names.DirPath.make [Libnames.coq_root] in
 
   (* ML includes *)
-  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in
-  List.map fst plugins_dirs,
+  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in
+
+  let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in
+
+  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 = "."
@@ -90,9 +103,7 @@ let libs_init_load_path ~coqlib =
   [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
-  (if Sys.file_exists user_contrib then
-     [build_userlib_path ~unix_path:user_contrib] else []
-  ) @
+  contrib_vo @
 
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
-  List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath)
+  List.concat misc_vo