diff options
| author | Hugo Herbelin | 2021-04-04 20:20:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-04 20:20:01 +0200 |
| commit | 643c10a894c1db24dd8ab06cc4376c92ae8b7c3c (patch) | |
| tree | f9987f68d20e4d4937c0424829bc5b8f6472a9ee /kernel/type_errors.ml | |
| parent | 950015d13ceb0c65c2eda42578788c8fe7ea31f1 (diff) | |
More extraction tests for inductive types with let-ins.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions