The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Dear Coq clubbers,

The Coq development team is pleased to announce the release of Coq 
8.9.0, available at

    https://coq.inria.fr/download

Source, as well as installers for Windows and MacOS, are available at

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

OPAM packages are available too.

There are no major changes with respect to 8.9+beta1. Major changes with 
respect to 8.8 are as follows:

Kernel: mutually recursive records are now supported.

Notations:

- Support for autonomous grammars of terms called "custom entries".

- Deprecated notations of the standard library will be removed in the 
next version of Coq, see the CHANGES.md file for a script to ease porting.

- Added the Numeral Notation command for registering decimal numeral 
notations for custom types.

Tactics: introduction tactics intro/intros on a goal that is an 
existential variable now force a refinement of the goal into a dependent 
product rather than failing.

Decision procedures: deprecation of tactic romega in favor of lia and 
removal of fourier, replaced by lra which subsumes it.

Proof language: focusing bracket "{" now supports named goals, e.g. 
"[x]:{" will focus on a goal (existential variable) named x.

SSReflect: the implementation of delayed clear was simplified: the 
variables are always renamed using inaccessible names when the clear 
switch is processed and finally cleared at the end of the intro pattern. 
In addition to that, the use-and-discard flag "{}" typical of rewrite 
rules can now be also applied to views, e.g. "=> {}/v" applies v and 
then clears v.

Vernacular:

- Experimental support for attributes on commands as in "#[local] Lemma 
foo : bar." Tactics and tactic notations now support the deprecated 
attribute.

- Removed deprecated commands Arguments Scope and Implicit Arguments in 
favor of Arguments.

- New flag Uniform Inductive Parameters to avoid repeating uniform 
parameters in constructor declarations.

- New commands Hint Variables and Hint Constants for controlling the 
opacity status of variables and constants in hint databases. It is 
recommended to always use these commands after creating a hint databse 
with Create HintDb.

- Multiple sections with the same name are now allowed.

Library: additions and changes in the VectorDef, Ascii, and String 
libraries. Syntax notations are now available only when using Import of 
libraries and not merely Require (source of incompatibility, see 
CHANGES.md for details).

Toplevels: coqtop and coqide can now display diffs between proof steps 
in color, using the Diffs option.

Tools: removed the gallina utility and the homebrewed Emacs mode.

Packaging: as in Coq 8.8.2, the Windows installer now includes many more 
external packages that can be individually selected for installation.