Merge PR #8958: [clib] Remove unneeded `get_extension` function.

3 files changed, 1 insertions, 9 deletions

diff --git a/clib/cUnix.ml b/clib/cUnix.ml
index 6b42e3041d..eedd878f93 100644
--- a/clib/cUnix.ml
+++ b/clib/cUnix.ml
@@ -74,10 +74,6 @@ let canonical_path_name p =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
-let get_extension f =
-  let pos = try String.rindex f '.' with Not_found -> String.length f in
-  String.sub f pos (String.length f - pos)
-
 let correct_path f dir =
   if Filename.is_relative f then Filename.concat dir f else f
 
diff --git a/clib/cUnix.mli b/clib/cUnix.mli
index 1b185345be..896ccd4ea7 100644
--- a/clib/cUnix.mli
+++ b/clib/cUnix.mli
@@ -38,10 +38,6 @@ val path_to_list : string -> string list
     [file] does not already end with [suf]. *)
 val make_suffix : string -> string -> string
 
-(** Return the extension of a file, i.e. its smaller suffix starting
-    with "." if any, or "" otherwise. *)
-val get_extension : string -> string
-
 val file_readable_p : string -> bool
 
 (** {6 Executing commands } *)
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml
index d0b01453a0..7395654022 100644
--- a/lib/coqProject_file.ml
+++ b/lib/coqProject_file.ml
@@ -220,7 +220,7 @@ let process_cmd_line orig_dir proj args =
       let f = CUnix.correct_path f orig_dir in
       let proj =
         if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
-        else match CUnix.get_extension f with
+        else match Filename.extension f with
           | ".v" ->
             { proj with v_files = proj.v_files @ [sourced f] }
         | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }