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 Coq
8.8.0, available at:

https://coq.inria.fr/download

Source, Windows and OS X packages are available at:

https://github.com/coq/coq/releases/tag/V8.8.0

Nix and OPAM packages are also available.

This release includes:

- Kernel: fix a subject reduction failure due to allowing fixpoints on
non-recursive values (#407), by Matthieu Sozeau. Handling of evars in
the VM (#935) by Pierre-Marie Pédrot.

- Notations: many improvements on recursive notations and support for
destructuring patterns in the syntax of notations by Hugo Herbelin.

- Proof language: tacticals for profiling, timing and checking success
or failure of tactics by Jason Gross. The focusing bracket ``{``
supports single-numbered goal selectors, e.g. ``2:{``, (#6551) by Théo
Zimmermann.

- Vernacular: cleanup of definition commands (#6653) by Vincent Laporte
and more uniform handling of the ``Local`` flag (#1049), by Maxime
Dénès. Experimental ``Show Extraction`` command (#6926) by Pierre
Letouzey. Coercion now accepts ``Prop`` or ``Type`` as a source (#6480)
by Arthur Charguéraud. ``Export`` modifier for options allowing to
export the option to modules that ``Import`` and not only ``Require`` a
module (#6923), by Pierre-Marie Pédrot.

- Universes: many user-level and API level enhancements: qualified
naming and printing, variance annotations for cumulative inductive
types, more general constraints and enhancements of the minimization
heuristics, interaction with modules by Gaëtan Gilbert, Pierre-Marie
Pédrot and Matthieu Sozeau.

- Library: Decimal Numbers library (#6599) by Pierre Letouzey and
various small improvements.

- Documentation: a large community effort resulted in the migration of
the reference manual to the Sphinx documentation tool. The new
documentation infrastructure (based on Sphinx) is by Clément
Pit-Claudel. The migration was coordinated by Maxime Dénès and Paul
Steckler, with some help of Théo Zimmermann during the final integration
phase. The 14 people who ported the manual are Calvin Beck, Heiko
Becker, Yves Bertot, Maxime Dénès, Richard Ford, Pierre Letouzey, Assia
Mahboubi, Clément Pit-Claudel, Laurence Rideau, Matthieu Sozeau, Paul
Steckler, Enrico Tassi, Laurent Théry, Nikita Zyuzin.

- Tools: experimental ``-mangle-names`` option to coqtop/coqc for
linting proof scripts (#6582), by Jasper Hugunin.

More information can be found in the CHANGES file. Feedback and bug
reports are extremely welcome.

Version 8.8 is the third release of Coq developed on a time-based
development cycle. Its development spanned 6 months from the release of
Coq 8.7 and was based on a public roadmap. The development process was
coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
release process.

The Coq Development Team

Attachment: signature.asc
Description: OpenPGP digital signature