The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Dear Coq-Club members,

We are pleased to announce that a second beta-release of Coq 8.4 is
available at http://coq.inria.fr/coq-84. Since the first beta release,
the main changes are

- Many fixes and improvements concerning "existential variables", 
  taking advantage of the new proof engine. For instance, a new command
  "Grab Existential Variables" allows to transform into goals the unresolved
  existential variables at the end of a proof.

- A unified framework now handles the backtracking commands of Coq
  (such as Reset, Back, BackTo, Backtrack or the "up" button of CoqIDE).
  The behavior of these commands may have slightly changed, more details
  in the documentation. As side-effects, a basic "Show Script" command
  has been reintroduced, and CoqIDE now correctly handles commands such as
  Restart, Abort, Undo.

- To mitigate the lack of a "info" tactical in 8.4, some verbose variants of
  specific tactics are now available : info_auto, info_eauto, info_trivial.
  Verbosity can also be activated by some Set/Unset commands.

A more detailed list of changes and bug fixes can be found in CHANGES
or via "svn log" or "git log" on the various Coq source repositories.
The main changes since 8.3 are described at http://coq.inria.fr/coq-84.

Please keep in mind that that this release is still a beta:
many bugs have been fixed since the first beta, but some remain
to be addressed. Nevertheless, we believe that this release is already
quite usable, and we strongly encourage you to give it a try.
By the way, a big thank to all our early testers and code contributers!

The coq dev team