We are happy to announce the first beta release of Coq 8.12.
This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. See the changelog for details.
As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the updated reference manual.
The 8.12 improvements to the reference manual are the start of an effort to improve Coq documentation. We believe the documentation needs considerable work to better serve the needs of the Coq community. Better documentation will encourage more people to learn, teach and use Coq. We need your help for this. We’re looking for volunteers who will help rewrite or add new material (such as better explanations and new examples) to the new pages. Writers do not have to be experts on their topic: we can pair writers with experts that can answer questions and provide examples. Indeed, it’s a great way to learn more about Coq. We’d also appreciate specific feedback, perhaps detailed, on what needs to be improved, what’s missing and what things to improve first. If you are willing to help, please see the dedicated wiki page to learn more.
Emilio and Théo, your 8.12 release managers