Merge pull request #873 from SkySkimmer/no-ml-cwd

Adapt to coq/coq#19834 (removal of Loadpath.has_ml field)

controller-js/coq_lsp_worker.ml

@@ -155,20 +155,13 @@ let main () =
   let stdlib coqlib =
     let unix_path = Filename.concat coqlib "theories" in
     let coq_path = Names.(DirPath.make [ Id.of_string "Stdlib" ]) in
-    Loadpath.
-      { unix_path; coq_path; implicit = true; has_ml = false; recursive = true }
+    Loadpath.{ unix_path; coq_path; implicit = true; recursive = true }
   in
 
   let user_contrib coqlib =
     let unix_path = Filename.concat coqlib "user-contrib" in
     let coq_path = Names.DirPath.empty in
-    Loadpath.
-      { unix_path
-      ; coq_path
-      ; implicit = false
-      ; has_ml = false
-      ; recursive = true
-      }
+    Loadpath.{ unix_path; coq_path; implicit = false; recursive = true }
   in
 
   let cmdline =

coq/args.ml

@@ -39,7 +39,6 @@ let ocamlpath =
 let coq_lp_conv ~implicit (unix_path, lp) =
   { Loadpath.coq_path = Libnames.dirpath_of_string lp
   ; unix_path
-  ; has_ml = true
   ; implicit
   ; recursive = true
   }

coq/workspace.ml

@@ -89,14 +89,14 @@ let compare = Stdlib.compare
 let coq_root = Names.DirPath.make [ Libnames.coq_root ]
 let default_root = Libnames.default_root_prefix
 
-let mk_lp ~has_ml ~coq_path ~unix_path ~implicit =
-  { Loadpath.unix_path; coq_path; has_ml; implicit; recursive = true }
+let mk_lp ~coq_path ~unix_path ~implicit =
+  { Loadpath.unix_path; coq_path; implicit; recursive = true }
 
 let mk_stdlib ~implicit unix_path =
-  mk_lp ~has_ml:false ~coq_path:coq_root ~implicit ~unix_path
+  mk_lp ~coq_path:coq_root ~implicit ~unix_path
 
 let mk_userlib unix_path =
-  mk_lp ~has_ml:true ~coq_path:default_root ~implicit:false ~unix_path
+  mk_lp ~coq_path:default_root ~implicit:false ~unix_path
 
 let getenv var else_ = try Sys.getenv var with Not_found -> else_
 
@@ -193,7 +193,7 @@ let make ~cmdline ~implicit ~kind ~debug =
   }
 
 let pp_load_path fmt
-    { Loadpath.unix_path; coq_path; implicit = _; has_ml = _; recursive = _ } =
+    { Loadpath.unix_path; coq_path; implicit = _; recursive = _ } =
   Format.fprintf fmt "Path %s ---> %s"
     (Names.DirPath.to_string coq_path)
     unix_path
@@ -340,7 +340,6 @@ let workspace_from_coqproject ~cmdline ~debug cp_file : t =
      *   (Printf.sprintf "Path from _CoqProject: %s %s" unix_path.path coq_path); *)
     { implicit
     ; recursive = true
-    ; has_ml = false
     ; unix_path = unix_path.path
     ; coq_path = dirpath_of_string_exn coq_path
     }