coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Release of Coq 8.10.1

From: Vincent Laporte <vincent.laporte AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Release of Coq 8.10.1
Date: Mon, 28 Oct 2019 10:44:37 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vincent.laporte AT gmail.com; spf=Pass smtp.mailfrom=vincent.laporte AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f53.google.com
Ironport-phdr: 9a23:qDjDpxeLgxF3qnzb26MqP4NklGMj4u6mDksu8pMizoh2WeGdxcS6YB7h7PlgxGXEQZ/co6odzbaP6OaxCCdZsN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6twHcu80ZjYd/Lqs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJxwIDab4+aO/ViZa7dcs8WSHBGUMpNWSFMAIWxZJYPAeobOuZYqpHwqFQPrRu4GQajGuXvyiNVjXHwx6I6y+MhERva3AM+AtkDt2rUrNTzNKgOT++1yrXIwS/Hb/xMwTf975LIcgw/rvyXUrJwdNDeyUgrFw/fklqQronlMiqT2+8QvWab6O9gWviui24hswxxrTmvxtssionUnY0Z0EzL9SJ8wIszONa2S1Z7bMa6HJdMsyyWLYh7T8M4T212pio216cKtJ61cSQS1ZgqyQPTZ+aZf4WI7R/vTvidLDdmiH5/Zb6yiBe//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CCSvRn/0eh3S+D1g7J6u1ZOEw0m6rWJpA7zr4/kZoTtkvDHivol0nskKCWcUAk9vCp6+ThfLrmuoeRO5Fohgz6KKgjmcyyDf4mPgQQQmSX4+Sx2bP78U38WrpKj/k2kqfDsJDdIMQWvrC5Aw5T0ok/9Rm/CSum3M4cnXYdNFJFfwiHj5T3NFzVL/D4CO2wg1WokDtx2//GObjhDo3XLnffiLfhYap960lExQUvytBf/otYBa0FIPLuQUD8r8fYDx88Mwys2enrEtR91oUEWWKOGKCVKq3SsUXbrt4oduKLfcoevCv3A/kj/f/ny3EjynEHeqz845oRY32+ArxCKl2ee2bhyoMfEGEBswwiCujjkFqYTTN7aHO7XqZ67TY+XtH1RbzfT5yg1eTSlBywGYdbMzgfVgK8VEzwfoDBYM8iLTqIK5Y4wDMBXLmlDYQm0EP27V6o+/9cNuPRvxYgm9fm3dlx6ffUkEhrpzNxBsWZlWqKSjMtxz5ad3oNxKl65HdF5BKD3Kx/2aEKENVS47ZWSF5/O8OHieN9DN/2V0TKedLbEFs=

Dear Coq users,

The version 8.10.1 of Coq has been released. Pre-compiled binaries for
macOS and MS-Windows (x86 and x86_64) can be downloaded from the
“release” page:
https://github.com/coq/coq/releases/tag/V8.10.1
It is also available through the OPAM and nixpkgs package repositories.

This new minor version brings a few bug fixes and documentation
improvements, in particular:

- Fix proof of False when using SProp
- Fix an anomaly when unsolved evar in Add Ring
- Fix Ltac regression in binding free names in uconstr
- Fix handling of unicode input before space
- Fix custom extraction of inductives to JSON

Feedback and bug reports are extremely welcome.
--
Vincent Laporte.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Release of Coq 8.10.1, Vincent Laporte, 10/28/2019