diff options
| author | coqbot-app[bot] | 2021-04-05 12:16:42 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-05 12:16:42 +0000 |
| commit | 56c32d83cb98056492b6d1feae800bbd73d1996a (patch) | |
| tree | f9987f68d20e4d4937c0424829bc5b8f6472a9ee /kernel/modops.ml | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
| parent | 643c10a894c1db24dd8ab06cc4376c92ae8b7c3c (diff) | |
Merge PR #13624: Fixing #13581: missing support for let-ins in arity of inductive types for extraction
Reviewed-by: pi8027
Diffstat (limited to 'kernel/modops.ml')
0 files changed, 0 insertions, 0 deletions