coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.12.0 is out!

From: Théo Zimmermann <theo AT irif.fr>
To: Coq Club <coq-club AT inria.fr>, coq+announcements AT discoursemail.com
Subject: [Coq-Club] Coq 8.12.0 is out!
Date: Mon, 27 Jul 2020 20:04:16 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:9un7lBP5cMCYFCfpja0l6mtUPXoX/o7sNwtQ0KIMzox0K/z7p8bcNUDSrc9gkEXOFd2Cra4d1ayI6+u5AzRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLJ/IA+3oAnNucUanJVuJroswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKLCAy/n3JhcNsjaJbuBOhqAJ5w47Ie4GeKf5ycrrAcd8GWWZNW8BcWCtcDIOhdIsPF/QOMvpEr4fzoFsOqAGxBQiqBOjyzjNFiXv70ag83u88Ew/JwRYgEsoBv3rUotv7N7ocX/6pw6fH1jjDc+pW1C3h5ITUbhwso/eBVq9wf8rLzkkvEhvIgEuQqYv/ODOazucCs2me7+plS+2vkWsnpBt3ojip28whjZXJhoILxVDD7ih5wZw1Jdy2SEJhb96kCoJduieHPIR5Xs0sWXtnuDomyrIYo567ejAHxZApyhDQd/GJfImF7w/+WOieLzp1hnxrda6xiRu9/0at1u/xW8m03ltWrCdIkcTBu34R2xLc9sWKV/hw80Wl1DuJygvd5OZEIUUumqraLZ4s2rEwlpsPsUTDAy/5g1/6jK6Rdkk85+eo7PjoYrb4qZ+GLYN7lgb+MqE2lsywAOQ4LggOX3WA9uimyLLj+kj5TbNXhfM1iqnUqI3WKMAUq6KjHQNY0oku5wy+Aju7ytgUgHcKIVFddB6Zk4TkP0vCLfP4APulnVigjDRmy+rbMrDjBpjAKGXInq37crZn8UFczRI+zdBB6JJQDbEMOPHzWkjrtNzfCh82LRK0z/z6CNV714MeR3uDAreDP6PIsF+I/eAiL/OCZI8PoDr9Kv4l6ODyjXIhhFMQeaak0YEJZH24EflqOUSUbWf2jtscH2oHvRIyTOnwh12DVT5TaWyyX6U55jwjFIKmDZnMRoe2jbyAxie7H5NWanpIClCWCXvobZmLW+8QaCKOJc9siiALVb+4S4M4yR6usBL6xKF8I+rP+iwYsIrj28Jv6+3SkxEy7z10AN6H32GDVWEn1l8PEhQxxehUpVF3ggOI1rE9iPhFH/RS4elIW0E0L8iYh+d9EpP7XATGY9GCRVOrRMm9KT0wVdk23sUVbkN0GtHkhRfGjASwBLpAq7wKA6sG86fZ0mL0LsB7gyLa1KQmp1g8Q8UJO3fw1f03zBTaG4OcyxbRrK2tb6lJmXOUrTrR/S+1pEhdFTVIf+DFUHQYPBeErtPj4UfPUfmzD7U5dxNI08+Zde1EcI+x1AQUdLLYIN3bJlmJtSK1DBeMyKmLadu4en8c0mPTEhpdylxBzTO9LQE7QxyZjSfGFjU/R1P1Yk2q//Ms8H4=

Dear Coq users,

We are happy to announce the release of Coq 8.12.0.

Some highlights from this release are:
- a new binder notation for non-maximal implicit arguments;
- an improved Search command which accepts more complex queries;
- many additions to the standard library;
- a restructured reference manual;
- the deprecation of the omega tactic in favor the lia tactic.

Please see the changelog to learn more about this release:
https://coq.github.io/doc/v8.12/refman/changes.html#version-8-12

Thanks to the reactivity of Coq users, this version is already
available in many packaging systems. In particular, it is already
available on opam and as a Docker image
(https://hub.docker.com/r/coqorg/coq/).

You may find the Windows and macOS installers on GitHub:
https://github.com/coq/coq/releases/tag/V8.12.0

The 8.12 release managers, Emilio and Théo, and the whole Coq development team

[Coq-Club] Coq 8.12.0 is out!, Théo Zimmermann, 07/27/2020