diff options
| author | Emilio Jesus Gallego Arias | 2018-05-05 22:06:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-08 01:10:52 +0200 |
| commit | 2c52a8304ed2bab9fc110818160463f57ba8fccd (patch) | |
| tree | 67967b6914044b8cb22ffd838ef1a4246b5577d6 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions
