diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-05 22:06:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:10:52 +0200 |
| commit | 2c52a8304ed2bab9fc110818160463f57ba8fccd (patch) | |
| tree | 67967b6914044b8cb22ffd838ef1a4246b5577d6 /tools/coqdep_common.mli | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[coqdep] Minor cleanups.
- Remove inclusion of the `tactics` directory, this is coming from a
time loadable modules were found there, now all are under `plugins`.
- Remove 2 dependencies so we can bootstrap coqdep earlier.
- Use `Format` instead of `Printf` for printing.
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d0d793243..91d2b4587 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -10,6 +10,8 @@ module StrSet : Set.S with type elt = string +val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a + (** [find_dir_logpath dir] Return the logical path of directory [dir] if it has been given one. Raise [Not_found] otherwise. In particular we can check if "." has been attributed a logical path |