Skip to content

@vbgl vbgl released this May 15, 2019 · 408 commits to v8.10 since this release

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).
Assets 6