diff options
| author | Gaëtan Gilbert | 2018-08-23 10:59:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 14:03:04 +0200 |
| commit | b3577d942307c3a23aabd224a588af16a0337094 (patch) | |
| tree | 5529d92eed92dddb1129db6354a59e5b8cd135e2 /plugins | |
| parent | e8937bfe903c7acbdfaa9d65bc0f5aaaa74a2bae (diff) | |
Elaboration: do not ask poly inductives to be template
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions