Skip to Content.
Sympa Menu

coq-club - [Coq-Club] [ANN] Mtac2 1.1 is out!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [ANN] Mtac2 1.1 is out!


Chronological Thread 
  • From: Jan-Oliver Kaiser <janno AT mpi-sws.org>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] [ANN] Mtac2 1.1 is out!
  • Date: Tue, 12 Feb 2019 15:59:02 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=janno AT mpi-sws.org; spf=Pass smtp.mailfrom=janno AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
  • Autocrypt: addr=janno AT mpi-sws.org; prefer-encrypt=mutual; keydata= mQENBFNx+loBCAC52t5xTWGjj9DMTCyTP3vL0cLh63ZNGTD7Ut5F3zVEyA1wlCRziuDVg+4b 7U7UBd2GpE4tY0YzRMlQElFP7XpkkEXC+JY+Vnor+4GyHvvbvRLKaB6mbQTsZ5R7I0O1gOy4 yCvljA9NrnFUI4f2HIZyOnjjgXlGjs4JgYCes/hgfvCLmtWq7Gve9xtEGq4IEKw9qz07Homh ExBDCwx8nfVphUnnt+PosxJuO/7rFN2v6wdL8PeQFMUsm9MADpNssuvSI+XC0QO0cK45g1zb ZTpaAzc3dXTjYjZm5tLo6ChWI8QpZRCfJUztaLIWiPd2NZLyr5OoM6HnUaj5vJZrEa4ZABEB AAG0JUphbi1PbGl2ZXIgS2Fpc2VyIDxqYW5ub0BtcGktc3dzLm9yZz6JAT0EEwEIACcFAlYF am0CGyMFCQlmAYAFCwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQWS0XeAYhTVyKXwf9EMDw f8rjZUSO29LYZgPdyneLkJ0oo/a0d59JRBap1BOkcXl3u0O78Ent74oZGra6ApAhNnfSmR6O pCaeTi/ePKslaHlw+PXZkpRtP7CCf3J0HTaTFjhA6NiTqBCO5hWEnzqpPukWKPacEhhAkW7S mrvWQiCsACiuISLyfp9S2qCEiL/bQcVQueD2qhWAwdiW18XdZOSfQlZ5iy93LMo8XNSKUrZL p7BU8478ntopp2Fx816pGMq7sJX4m0hQBikEXL9SBtINAY8mw9KNzxMOvhSMbAe13UbAFOQp L3aIy7RgbttIHLQZ0djwXUmAQrmMK0pIM8itge2wE4CNzwJbW7kBDQRTcfpaAQgAxT/Y3kod hYL5gHQNPSgICwK4czJ2bPc7JTbJjtHcA7SLRNFeQc/krjD4NCmoRIhTFQUI0WBNtzyiewcd 8cZV2BCB6CqqviFhzkzld+j22HT8glgWDEVuK37rHscdFAceva9jBVdd1Rn6cwwMjZ0EQK7R vxGkuAApHXoZyV+Xbh+dzvypv+EAU2o3lq04cdU8kogXNgbzGSUrEV2ilrF4O2SGYDnvAo/y hnEgjjlHAd5o+XXfobClEuEUrsfsaw7hsd6QNvqVhIchoNtIvRoabHvIKi0KYviopzCtKGrn tPWOboR5drLKrWKJo4AFudvIdKie+3yO6OAhJ+dxHe776wARAQABiQElBBgBAgAPBQJTcfpa AhsMBQkJZgGAAAoJEFktF3gGIU1cs7kH/0F9wdpy9r2fQfs8JLudhROvPTJh/8wbiwTzUEf2 rLSK/LiE/FqhY+O4k6HzmwdqwnadfSZghT/N5Rir3B6O4zBmol7AZf5Idnq+pgAyDvetz4Dj LNSxLKKjYfKyANzAyg8S1c+Dsbv0BsHfmzlGxDxUCe5YooIdeVb7zueRxnWenkv5EFsbWO4y CwYRom8VVTjKYVtGK3yWOvY1SZlQHbXnpbTSUs5OTh7CS2HVoJZDpSqi0k2COwd/AaNGZ3Vf A3H6uGLk8vMUj7L4cfNkEORiUnhR8HUx+h1DIMt+gINO3L2TK36jg8QbUo+Bx5C6SiPqkVuT 281nL3ehPA5Z/Qo=
  • Ironport-phdr: 9a23:WHzWZhaVuGfOYmfGc4OlKhb/LSx+4OfEezUN459isYplN5qZoMW9bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAn8G/Zl89+gqxVrx2uuxNxzJXZYJ2XOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQFJ+lYqZDxqUIKrRu/GwmjGvnvwSJNiHDs3K06yPouERvb1wEnHdIBqnLUrNPyNKoJVOC11KjIwSzYb/JYwjfx8o/IcgouofyVW797bMTfyU4qFwzfj1WQr5ToPzaN1uQMqmSb9ORhVfm1h24gsQFxrSCjxsgtionVhoIV10vL+T9lz4YyIN21TlNwb928EJZIqi2XOY97Ttk/T2xsoio3ybwLtYS0cSQW0Jgr2hDSZvidf4SV5h/vTvudLDR3iX5/Zr6zmgi+/E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CFSvtg+Eeh3iyD1wXL6uFFOEw0lq7bK4U6zbIqk5oTqUvDEjXrl0rolKOWd0Mk9fa06+n/f7nrqJuRO5Vphgz6KKgjmc2yDf43PwQSR2Sb/P6z1Lzn/U33WrVKifg2n7HbsJ/AI8QboKm5DhRQ0oY76hazFiym0doDnXUdK1JFYh2Hg5DzO17SOPD4Eeu/g1O0nTh3wPDGJ6TtDYnJLnjei7jsZq196k5ZyAor199T/ZNUCrcbIPLyQED9rtLYDgVqezCzlqzsD8w43YcDU0qOBLWYOeXcqxXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKIug294wbHGmE+4uAEyYenf2yoMDGGEMuSI7VO2vk0KZFzlJaCDhDOoH+jgnBdf+Xs/4TYe3jenZhXbpLthtfmlDT2u0PzLtfoSAVe0LbXvJcMp5k3kfSqPnTJUuh0j36F3KjoF/J++RwRU28Ir53YEutejLlFQp6icyCN6SgTnUEjNE21gQTjpz55hR5ExwzlDZi/p6nvpfU9lL5rZKVhwwc5vEwKp2BoKqVw==
  • Openpgp: preference=signencrypt

We are proud to announce the official 1.1 release of Mtac2. This is part of an ongoing effort to provide an up-to-date plugin for Coq with the Mtac2 typed tactic language. Mtac2 is still under heavy development, but with a pretty stable core. As such, we decided to follow Coq's development process and package new releases with every Coq release.
The Mtac2 1.1 release is compatible with Coq 8.8 and 8.9. (The 1.0 release is compatible with Coq 8.7 and 8.8.)

We provide an opam package called "coq-mtac2".

This release includes, among several bug-fixes:

- Performance improvements mostly related to reducing the number of universes required for Mtac2 programs.
- A new primitive for creating inductive definitions (still in beta).
- A richer type for goals, which uses an inductive index to facilitate writing tactics. The new type also includes the possibility to change a hypothesis's type.

We are happy to take feedback in the form of GitHub issues in the https://github.com/Mtac2/Mtac2 repository. If you prefer a more direct form of communication, you can join our Mattermost:
https://mattermost.mpi-sws.org/iris/channels/mtac
(You can use your GitHub account to sign up for the Mattermost server.)

Happy tactic coding,
The Mtac2 team.


  • [Coq-Club] [ANN] Mtac2 1.1 is out!, Jan-Oliver Kaiser, 02/12/2019

Archive powered by MHonArc 2.6.18.

Top of Page