diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 23:38:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 23:38:32 +0100 |
| commit | c671d86beecb4e31ad5c7752f7e4fb570823e837 (patch) | |
| tree | 198cfdd80f336c585fef35aa94ba60c0ab5b8b2c /pretyping/tacred.mli | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Cleanup conditional in lint-repository.sh
Diffstat (limited to 'pretyping/tacred.mli')
0 files changed, 0 insertions, 0 deletions