Releases
The history of the Rocq Prover and its Platform releases with a summary and a complete changelog, as well as the manual at that time.
3 Releases
Coq Platform 2024.10.1
- For Coq 8.19.2
- Coq 8.12.2-8.18.0 available
- Compatibility with opam 2.3.0
Coq 8.20.0
- User-defined rewrite rules
- Primitive strings
- A lot of work went into reducing the size of the bytecode segment, which in turn means that .vo files might now be considerably smaller.
- A new version of the docker-keeper compiler to build and maintain Docker images of Coq.
Coq 8.19.2
- Sort polymorphism makes it possible to share common constructs over Type, Prop and SProp.
- The notation term%_scope to set a scope only temporarily (in addition to term%scope for opening a scope applying to all subterms).
- lazy, simpl, cbn and cbv and the associated Eval and eval reductions learned to do head reduction when given flag head.
- New Ltac2 APIs, improved Ltac2 exact and dynamic building of Ltac2 term patterns.
- New performance evaluation facilities: Instructions to count CPU instructions used by a command (Linux only) and Profiling system to produce trace files.
- New command Attributes to assign attributes such as deprecated to a library file.