aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-17 09:03:09 +0200
committerMaxime Dénès2017-05-17 09:03:09 +0200
commit5360ec8ff56c44e96c56965be78e6f2538963a57 (patch)
tree82361651080323e8ab33db31890c32b93f6928ea /tools
parent5ea95f9cd843bec4504646851bf22bf505e56ad8 (diff)
parent9ddfdab6a4715a08a78296bf8824d086f358bdc0 (diff)
Merge PR#636: Miscellaneous typos, dead code, etc.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep_common.ml7
-rw-r--r--tools/coqdep_common.mli3
2 files changed, 0 insertions, 10 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebdae..93b25e2ede 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -544,13 +544,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir =
let add_rec_dir_import add_file phys_dir log_dir =
add_directory true (add_file true) phys_dir log_dir
-(** -R semantic but only on immediate capitalized subdirs *)
-
-let add_rec_uppercase_subdirs add_file phys_dir log_dir =
- process_subdirectories (fun phys_dir f ->
- add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
- phys_dir
-
(** -I semantic: do not go in subdirs. *)
let add_caml_dir phys_dir =
add_directory false add_caml_known phys_dir []
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 633c474ada..10da0240dd 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -64,8 +64,5 @@ val add_rec_dir_no_import :
val add_rec_dir_import :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_uppercase_subdirs :
- (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-
val treat_file : dir -> string -> unit
val error_cannot_parse : string -> int * int -> 'a