coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.10.0

From: Vincent Laporte <vincent.laporte AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq 8.10.0
Date: Wed, 9 Oct 2019 15:27:39 +0000
Authentication-results: mail3-smtp-sop.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-f42.google.com
Ironport-phdr: 9a23:VvTHLxBuvYYXlZzLuhixUyQJP3N1i/DPJgcQr6AfoPdwSPT5p8bcNUDSrc9gkEXOFd2Cra4d0KyI6uu+BSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+NhS7oRjeusQXjoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RwgqxFvRyvpBJxzIDbb46JL/d+cb/RcMkdS2ZdUMtcVSpMCZ68YYsVCOoBOP5VoIb8p1sIsRSxGw+sBP/ywTFOnHD2xao60/49EQ7YwQctGMwOsHXSrNrpKqgSV/y1wLPMzTrZd/NW3i396JTWfR06rvGMWKh/ccvVyUU1CwzFiVCQpJXjMjiI2OoNtG2b4PBhVeKpk2MnqgdxoiKuxsg2kIXJiJgVxkjL9SV43IY1JcC4R1VhbdG4F5tQsieXPJZ1TMM6W2xkpjo2x7kctZO4fCUG0oorywDCZ/CdfIWE/ArvWPufLDtlnn5pZrKyihmo/US9yuDwTNe43EpJoydDj9LCrGoC1wbJ5ciCUvZ9/lmu2TKI1w3L7+FLO0E0la7CJ58v2L48i4MfsUrMEyPogkn2g6iWdkIr+uis9evreKnpppiZN4NsiwH+NLohmtCnDOgmLgQDW3KX9Oe82bH540H1XqhGguc5n6XHqJzaIN4Upq+9Aw9byIYj7BO/Ai+40NQZm3kIMExKeBSbj4TzP1HBOuj4DfClg1Swjjhm3P/GPrj7DZXMKnjPiqvufbF460JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4KvlimZ8klsAd4Go24EWYTa2BKdIOUKcNETthNwMF3tCmgMmS/b2hRXWTz9VbHu0Q+Q47yk8Ep6rJYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJUMX/AEopaijUBEIOZZcoh2BWp7lKozrNmKq/L4HRdu865ktdy4OLXmFc58jkmV53BgVHIdHl9myYzfxFzxLp2+BUvxVKK0Kw+iPtdR4QKtqF5FzwiPJuZ9NRUTtX7WwbPZNCMEQ/0TdCvADV3RdU0kYYD

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.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Coq 8.10.0, Vincent Laporte, 10/09/2019
- RE: [Coq-Club] Coq 8.10.0, Roger Witte, 10/09/2019
  - Re: [Coq-Club] Coq 8.10.0, Théo Zimmermann, 10/09/2019
    - Re: [Coq-Club] Coq 8.10.0, Roger Witte, 10/09/2019
      - RE: [Coq-Club] Coq 8.10.0, Roger Witte, 10/10/2019
        
        Re: [Coq-Club] Coq 8.10.0, Théo Zimmermann, 10/10/2019
        
        RE: [Coq-Club] Coq 8.10.0, Soegtrop, Michael, 10/10/2019
        
        Re: [Coq-Club] Coq 8.10.0, Théo Zimmermann, 10/10/2019
        RE: [Coq-Club] Coq 8.10.0, Soegtrop, Michael, 10/10/2019
- Re: [Coq-Club] Coq 8.10.0, Xuanrui Qi, 10/09/2019
  - Re: [Coq-Club] Coq 8.10.0, Théo Zimmermann, 10/09/2019