Guillaume Melquiond
2018-11-06 09:46:14 UTC
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.
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.