diff options
| -rw-r--r-- | clib/cUnix.ml | 4 | ||||
| -rw-r--r-- | clib/cUnix.mli | 4 | ||||
| -rw-r--r-- | lib/coqProject_file.ml | 2 |
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] } |