diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-14 11:14:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-15 20:31:46 +0200 |
| commit | 9ddfdab6a4715a08a78296bf8824d086f358bdc0 (patch) | |
| tree | 35b10690d7c86d83047d6bac8792bb93bebb03d6 /tools/coqdep_common.mli | |
| parent | a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 (diff) | |
Dead code in coqdep.
Was introduced in 5268efdef, reverted then readded in 1be9c4d.
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 633c474ad..10da0240d 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 |