diff options
| author | Gaëtan Gilbert | 2018-08-22 17:43:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:21:00 +0200 |
| commit | 69339f8fcfe3e5f3fa1c58feba6b0740c7e86538 (patch) | |
| tree | f09548fade8a03d2fb12edc6f58964dd25627eb1 /dev/ci | |
| parent | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (diff) | |
Fix #7754: universe declarations on mutual inductives
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions