Revert "On MacOS X, ensuring that files found in the file system have the"

and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files"
and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X."

This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.

Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.

3 files changed, 5 insertions, 32 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index ac0b6f722..b0eed8386 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -39,25 +39,12 @@ let path_to_list p =
 let user_path () =
   path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
 
-  (* Duplicated from system.ml to minimize dependencies *)
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      String.equal df "." || String.equal df "/" ||
-      aux df && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
-
 let rec which l f =
   match l with
     | [] ->
       raise Not_found
     | p :: tl ->
-      if file_exists_respecting_case (p / f) then
+      if Sys.file_exists (p / f) then
 	p
       else
 	which tl f
@@ -115,7 +102,7 @@ let _ =
     If the check fails, then [oth ()] is evaluated. *)
 let check_file_else ~dir ~file oth =
   let path = if Coq_config.local then coqroot else coqroot / dir in
-  if file_exists_respecting_case (path / file) then path else oth ()
+  if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
   let prelude = "theories/Init/Prelude.vo" in
@@ -147,7 +134,7 @@ let coqpath =
   let coqpath = getenv_else "COQPATH" (fun () -> "") in
   let make_search_path path =
     let paths = path_to_list path in
-    let valid_paths = List.filter file_exists_respecting_case paths in
+    let valid_paths = List.filter Sys.file_exists paths in
     List.rev valid_paths
   in
   make_search_path coqpath
diff --git a/lib/system.ml b/lib/system.ml
index 27e21204c..d1cdd8efc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,18 +53,6 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      (String.equal df "." || String.equal df "/" || aux df)
-      && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
-
 let rec search paths test =
   match paths with
   | [] -> []
@@ -89,7 +77,7 @@ let where_in_path ?(warn=true) path filename =
   in
   check_and_warn (search path (fun lpe ->
     let f = Filename.concat lpe filename in
-    if file_exists_respecting_case f then [lpe,f] else []))
+    if Sys.file_exists f then [lpe,f] else []))
 
 let where_in_path_rex path rex =
   search path (fun lpe ->
@@ -105,7 +93,7 @@ let where_in_path_rex path rex =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
-    if file_exists_respecting_case filename then
+    if Sys.file_exists filename then
       let root = Filename.dirname filename in
       root, filename
     else
diff --git a/lib/system.mli b/lib/system.mli
index 051e92f16..a3d66d577 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -29,8 +29,6 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
-val file_exists_respecting_case : string -> bool
-
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]