github coq/coq V8.10+beta1
Coq 8.10+β1

latest releases: V8.19.1, V8.19.0, V8.19+rc1...
pre-release5 years ago

This is the first β version of Coq 8.10.

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.

Caveat: at the time of this writing, there are two known significant issues. You may get more information about them and track the work towards their resolution on the corresponding threads:

  • CoqIDE does not work properly on Windows (issue #9885);
  • Template polymorphism breaks Prop/Set separation (issue #9294, proposed fix #9918).

Don't miss a new coq release

NewReleases is sending notifications on new releases.