diff options
| author | Gaëtan Gilbert | 2018-08-23 10:54:19 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 14:03:04 +0200 |
| commit | e8937bfe903c7acbdfaa9d65bc0f5aaaa74a2bae (patch) | |
| tree | 75d9b7b0ec03713d2e2abd46ec24e745d8a2fae9 /plugins | |
| parent | c3b71e45db77f0875a8080275c6a1ae4b353d68d (diff) | |
Elaboration: do not ask small inductives to be template
This doesn't change behaviour currently as the kernel also makes this
decision, but in the future it won't.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions