diff options
| author | Gaëtan Gilbert | 2020-01-17 14:32:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 13:13:24 +0100 |
| commit | d81375002501cdc6e677244557a87b2f1a445e5b (patch) | |
| tree | 45e3f1f5a93e9676952637eec853a510f25f2919 /dev | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
Check instance length in type_of_{inductive,constructor}
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions