The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Dear Coq-Club,

The reference manual for the beta version of Coq 8.9 is available at:
https://coq.inria.fr/distrib/V8.9+beta1/refman

You may notice error messages in Coq snippets. There is currently no
infrastructure for detecting those (see also
https://github.com/coq/coq/issues/7755) thus if you notice some error
messages, we would really like that you open bug reports (except in the
cases where it's clear from the context that the error was expected), or
even better that you submit a pull request fixing the problem (use the
"Edit on GitHub" button and here is some documentation on getting
started with Sphinx:
https://github.com/coq/coq/tree/master/doc/sphinx#documenting-coq-with-sphinx;
fixing the kind of problem I am mentioning is generally a matter of
adding a `reset` at the right `.. coqtop::` directive as explained here
https://github.com/coq/coq/tree/master/doc/sphinx#coq-directives).

Thanks,
Théo

On 06/11/2018 10:46, Guillaume Melquiond wrote:
> 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.

Attachment: signature.asc
Description: OpenPGP digital signature