| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-08 | remove `with hintdb` variant of Ltac2 `unify`, because | Samuel Gruetter | |
| passing one single hintdb is not quite the right API, we should pass a transparent state instead, but that would require an API for manipulating hintdbs and transparent states, postponing | |||
| 2021-04-07 | unify for Ltac2 | Samuel Gruetter | |
| Fixes #14083 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |