diff options
| author | Pierre-Marie Pédrot | 2018-05-10 20:46:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-10 20:46:19 +0200 |
| commit | 5da17b8c60846913db18b0f9216d63898933aa52 (patch) | |
| tree | 365f4b54a645e23f9f702eb7e343182dcac34179 /dev | |
| parent | e559f7553030dc3a86936794d0f80f39b0131960 (diff) | |
| parent | 818ba539cf4a0aed2172f370dcddd380b6ec6a4c (diff) | |
Merge PR #7437: [coqdep] Minor cleanups.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions