The Coq mailing list

[Roger Witte <Roger.Witte AT dft.gov.uk>]

I saw the announcement on the web site yesterday evening and tried a 
download.  I will download again this evening in case you have made fixes 
overnight. However my observations using CoqIde under windows so far are:
        -       The latex to Unicode input function stops working after a 
little while editing and compiling and then stays not working until I close 
the file
        -       The IDE doesn't play nicely with 'autohide toolbar' so 
although I can swap back and forth between CoqIde and other processes 
(character map and Chrome) using keyboard shortcuts, I cannot do so using the 
mouse when CoqIde is full screen in the foreground.
        -       The help menu is broken: The links to the reference manual 
and library documentation go to bad addresses, as does the link to coq home 
from the about dialog.

If you can tell me how to raise a bug report without logging in to github, I 
will happily do so but I don't want to join github.

Regards
Roger

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Vincent Laporte
Sent: 09 October 2019 16:28
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Coq 8.10.0

Dear Coq users,

The 8.10.0 release of Coq is available.

Main changes:

-   some quality-of-life bug fixes;
-   a critical bug fix related to template polymorphism;
-   native 63-bit machine integers;
-   a new sort of definitionally proof-irrelevant propositions: SProp;
-   private universes for opaque polymorphic constants;
-   string notations and numeral notations;
-   a new simplex-based proof engine for the tactics lia, nia, lra and nra;
-   new introduction patterns for SSReflect;
-   a tactic to rewrite under binders: under;
-   easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

All details can be found in the user manual:
https://coq.inria.fr/distrib/current/refman/changes.html#version-8-10

Pre-compiled binaries can be downloaded from the “release” page:
https://github.com/coq/coq/releases/tag/V8.10.0

Feedback and bug reports are extremely welcome.

--
Vincent Laporte.

__________________________________________________________________________________________
This email has originated from external sources and has been scanned by DfT’s 
email scanning service.
__________________________________________________________________________________________

**********************************************************************
The information in this email may be confidential or otherwise protected by 
law. If you received it in error, please let us know by return e-mail and 
then delete it immediately, without printing or passing it on to anybody else.
Incoming and outgoing e-mail messages are routinely monitored for compliance 
with our policy on the use of electronic communications and for other lawful 
purposes.