aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-14 11:14:43 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-15 20:31:46 +0200
commit9ddfdab6a4715a08a78296bf8824d086f358bdc0 (patch)
tree35b10690d7c86d83047d6bac8792bb93bebb03d6 /tools/coqdep_common.ml
parenta05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 (diff)
Dead code in coqdep.
Was introduced in 5268efdef, reverted then readded in 1be9c4d.
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebda..93b25e2ed 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 []