aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-05 12:16:42 +0000
committerGitHub2021-04-05 12:16:42 +0000
commit56c32d83cb98056492b6d1feae800bbd73d1996a (patch)
treef9987f68d20e4d4937c0424829bc5b8f6472a9ee /kernel/nativelib.ml
parent012b8a08f142d39b2211fd52c811f830f88f2075 (diff)
parent643c10a894c1db24dd8ab06cc4376c92ae8b7c3c (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/nativelib.ml')
0 files changed, 0 insertions, 0 deletions