Coq 8.10+beta1 is out
Submitted by Vincent Laporte on May 15th, 2019
The first beta release of Coq 8.10 is available for testing.
Coq version 8.10 contains two major new features: support for a native machine integer type and a new sort SProp, a definitionally proof irrelevant universe. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, cleanups of the internals of the system and API, and many documentation improvements. This release includes many user-visible changes, including deprecations and new features. A more detailed list of changes appears in the reference manual.
Feedback and bug reports are extremely welcome.