| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-26 | Add non-performance-based test | Jason Gross | |
| 2021-03-26 | Fix Ltac2 `Array.init` exponential overhead | Jason Gross | |
| Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |