Makefile: restore the use of coqdep_boot for creating .v.d files

 Coqdep_boot has almost no dependencies, and hence can be compiled
 very early during the build, without relying on .ml.d files.
 Some code of system.ml is now in a separate file minisys.ml,
 which is also included in system.ml for compatibility.

1 files changed, 1 insertions, 59 deletions

diff --git a/lib/system.ml b/lib/system.ml
index e54109a2f..ffb4459d7 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,65 +12,7 @@ open Pp
 open Errors
 open Util
 
-(** Dealing with directories *)
-
-type unix_path = string (* path in unix-style, with '/' separator *)
-
-type file_kind =
-  | FileDir of unix_path * (* basename of path: *) string
-  | FileRegular of string (* basename of file *)
-
-(* Copy of Filename.concat but assuming paths to always be POSIX *)
-
-let (//) dirname filename =
-  let l = String.length dirname in
-  if l = 0 || dirname.[l-1] = '/'
-  then dirname ^ filename
-  else dirname ^ "/" ^ filename
-
-(* Excluding directories; We avoid directories starting with . as well
-   as CVS and _darcs and any subdirs given via -exclude-dir *)
-
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
-  not (f = "") && f.[0] != '.' &&
-  not (List.mem f !skipped_dirnames) (*&&
-  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
-
-(* Check directory can be opened *)
-
-let exists_dir dir =
-  try Sys.is_directory dir with Sys_error _ -> false
-
-let check_unix_dir warn dir =
-  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
-    (String.length dir > 2 && dir.[1] = ':' ||
-     String.contains dir '\\' ||
-     String.contains dir ';')
-  then warn ("assuming " ^ dir ^
-             " to be a Unix path even if looking like a Win32 path.")
-
-let apply_subdir f path name =
-  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
-  (* as well as skipped files like CVS, ... *)
-  if ok_dirname name then
-    let path = if path = "." then name else path//name in
-    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
-    | Unix.S_DIR -> f (FileDir (path,name))
-    | Unix.S_REG -> f (FileRegular name)
-    | _ -> ()
-
-let readdir dir = try Sys.readdir dir with any -> [||]
-
-let process_directory f path =
-  Array.iter (apply_subdir f path) (readdir path)
-
-let process_subdirectories f path =
-  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
-  process_directory f path
+include Minisys
 
 (** Returns the list of all recursive subdirectories of [root] in
     depth-first search, with sons ordered as on the file system;