The Coq mailing list

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

Dear Coq users,

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

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

Source, Windows and OS X packages are available.

The main changes 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.

Documentation: we integrated a large number of fixes to the new Sphinx 
documentation.

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.

Version 8.9 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system.  Most
important ones are documented in the CHANGES.md file.