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.8, available at:

https://github.com/coq/coq/releases/tag/V8.8%2Bbeta1

Source, Windows and OS X packages are available.

Summary of changes:

- 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.

- 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