The Coq mailing list

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

Dear coq-clubists,

8, 4, 2, Ready, Go ! After this binary countdown, I'm glad to announce
the availability of Coq 8.4, 2nd revision. Sources and Windows packages 
are already on coq.inria.fr. MacOS packages are still underway (see [1]).

As usual, a fair amount of bugs have been solved since the last release,
but not all alas :-(, see CHANGES below or the bugzilla summary [2].
We'd like to thank all contributors and bug submitters. Among them,
I would like to personally thank Andrew Appel for his help during
the resolution of a nasty issue with the interrupt button of Coqide
for Windows (bug #2869).

Enjoy!
Pierre Letouzey, for the Coq Dev Team

[1] https://sympa.inria.fr/sympa/arc/coq-club/2013-01/msg00081.html

[2] Bugs resolved since last release (all versions, not only 8.4):
https://coq.inria.fr/bugs/buglist.cgi?list_id=769&chfieldto=Now&query_format=advanced&chfield=bug_status&chfieldfrom=2012-12-25&chfieldvalue=RESOLVED&bug_status=RESOLVED


--------------------------------------------------------------------------
Changes from V8.4pl1 to V8.4pl2
===============================

Bug fixes

- Solved bugs :
  #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967
  #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 
- Partially fixed bugs : #2830 #2949
- Coqtop should now react more reliably when receiving interrupt signals:
  all the "try...with" constructs have been protected against undue
  handling of the Sys.Break exception.

Coqide

- The Windows-specific code handling the interrupt button of Coqide
  had to be reworked (cf. bug #2869). Now, in Win32 this button does
  not target a specific coqtop client, but instead sends a Ctrl-C to
  any process sharing its console with Coqide. To avoid awkward
  effects, it is recommended to launch Coqide via its icon, its menu,
  or in a dedicated console window.

Extraction

- The option Extraction AccessOpaque is now set by default,
  restoring compatibility of older versions of Coq (cf bug #2952).