aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_13581.v
AgeCommit message (Expand)Author
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04Fixing #13581: missing support for let-ins in arity of inductive types.Hugo Herbelin