The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Dear Coq Clubbers,

  The Coq development team is pleased to announce the release of the
first beta version of Coq 8.6, available at:

http://coq.inria.fr/coq-86

Source, Windows and OS X packages are available.

This release includes:

- A new, faster state-of-the-art universe constraint checker by
  Jacques-Henri Jourdan.
- In CoqIDE and other asynchronous interfaces, more fine-grained
  asynchronous processing and error reporting by Enrico Tassi, making
  Coq capable of recovering from errors and continuing to process the
  document.
- Better access to the proof engine features from Ltac: goal management
  primitives, range selectors and a typeclasses eauto engine handling
  multiple goals and multiple successes, by Cyprien Mangin, Matthieu
  Sozeau and Arnaud Spiwack.
- Tactic behavior uniformization and specification, generalization of
  intro-patterns by Hugo Herbelin and others.
- A brand new warning system allowing to control warnings, turn them
  into errors or ignore them selectively by Maxime Dénès, Guillaume
  Melquiond, Pierre-Marie Pédrot and others.
- Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
- The ssreflect subterm selection algorithm by Georges Gonthier and
  Enrico Tassi, now accessible to tactic writers through the
  ssrmatching plugin.
- LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico
  Tassi and Tobias Tebbi.

See http://coq.inria.fr/ and the CHANGES file in the distribution for
for more details.

Coq 8.6 initiates a time-based release cycle, with a major version being
released every 10 months. The roadmap is also made public.

To date, Coq 8.6 contains more external contributions than any previous
Coq version. Code reviews were systematically done before integration
of new features, with an important focus given to compatibility and
performance issues.

The Coq Development Team