| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-15 | Fixes #12348: long-standing de Bruijn indices bug in imitation ↵ | Hugo Herbelin | |
| (solve_simple_eqn). The bug was that an assumption could be interpreted as a local definition and wrongly expanded. It triggered rarely because it involved mixing let-ins and local assumptions + imitation under binders. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |