| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-22 | Clarify Global.env usage in ppvernac | Gaëtan Gilbert | |
| 2019-05-10 | [api] Remove 8.10 deprecations. | Emilio Jesus Gallego Arias | |
| Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it. | |||
| 2019-03-20 | Stop accessing proof env via Pfedit in printers | Maxime Dénès | |
| This should make https://github.com/coq/coq/pull/9129 easier. | |||
| 2018-12-11 | [api] Move reduction modules to `tactics` | Emilio Jesus Gallego Arias | |
| These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |