ceps
ceps copied to clipboard
coq
Coq Enhancement Proposals
In particular, the proposed syntax has: - pattern selection for all reductions - support for fine-tuning iota by enabling/disabling specific constructor names - support for referring to unfolding databases as...
This is a CEP to discuss the technical details of the corresponding point of the roadmap https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md Rendered: https://github.com/proux01/ceps/blob/boost-stdlib-dev/text/083-boost-stdlib-dev/text.md
[Rendered](https://github.com/coq/ceps/blob/01e72cde228917872bf1c3f70dee58fc9a16e6f7/text/086-reduce-barriers-to-contributing-to-stdlib.md)
This is a draft PR for now because each item in the list should be completed with some more precise description of what they mean, what the planned outcomes are,...
[Rendered](https://github.com/herbelin/ceps/blob/global-fixpoints/text/global-fixpoints.md)
Is there a consensus as to what "The Rocq Prover" translates to in French ? "Le prouveur Rocq", "Rocq", "The Rocq prover", still Coq ? Best, MRandl
Rendered [here](https://github.com/herbelin/ceps/blob/master+match-with-alias/text/match-with-alias.md).
Rendered: https://github.com/Villetaneuse/ceps/blob/clean_up_Reals/text/000-clean-up-Reals.md
