coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.6 is out!

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.6 is out!
Date: Wed, 21 Dec 2016 10:18:53 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:cJR5FBZvN5N+hm+yrNq63fz/LSx+4OfEezUN459isYplN5qZoMm6bnLW6fgltlLVR4KTs6sC0LuN9fC4EjVbud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ihi6twbcutUZjYd/JKs91gbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyvpxJx3ZPaboKbNPVxYqzSYNwUSmhPUctKSyxMAZmxY5cTA+cbP+tVqZT2qVsUrRu5AAmhHOzhyjlShn/3waI61PkqHx/c0ww7BNIOsWnfodLrO6cUS+C1zbXHzTLZY/NKwzj985PIchE6rPGNW7Jwa8vRxlM1GwPLlFWdsIroNC6b2OQKtmiU9etgVeS3hm4oqgFxvjivxto3hYXTmo0VzVXE+CNky4g2Pd21UEp2bNG+HJdOuSyWLYp7T8c4T211pio3yKUKtYO1cSUJ0pgqwx/SZ+aZf4SU/h7vTuacLDZ+iXl4YrywnQyy/lKlyuDkVsm7zlJKri1dn9nCqH8NywDT6tWBSvth5EitwzGP1xrc6u1cIEA0k7TUK4I5z7M0mZcfq1rPEyHslEj3iKKabFgo9vaq5uj/Z7XpvJ6cN4t6igHkNaQun9SyAesiPQgUQWeb4v+x1LP98k3lXLVKk/s2krXDv5zAIsQbvKG5DxdP0ok/8xa/Eyum0NMAkHYbK1JFYQuLgJTtO1HTO//1Fuy/glSpkDdz3f/KJLzhApPXLnjCirjtZ7h961QPgDY0mNtY/tdfDqwLCPP1QE748tLCXTEjNAnh7uD9Cd56nr8XQnmOSvuUNrnTuljO+us0OOikZYkPuT+7JeJztK2mtmMwhVJIJfrh5pAQcn3tRvk=

On Tue, Dec 20, 2016 at 11:24:09AM +0100, Ralf Jung wrote:
> Hi,
>
> > It is, however it sadly lacks CoqIde and SSreflect:
> >
> > /The following actions will be performed:/
> > / ⊘ remove coqide 8.5.3 [conflicts with
> > coq]/
> > / ⊘ remove coq-mathcomp-ssreflect 1.6 [conflicts with
> > coq]/
> > / ↗ upgrade coq 8.5.3 to 8.6/
> > /===== ↗ 1 ⊘ 2 =====/
> > /Do you want to continue ? [Y/n] n/
>
> Not sure about coqide, but for ssreflect, I am using the "dev" version
> from <https://github.com/coq/opam-coq-archive>.

I'll do my best to release a 1.6.1 version of coq-mathcomp-* in order
to make it possible to use mathcomp 1.6 on Coq 8.6 without pulling in
the dev repositories/packages.

Ciao
--
Enrico Tassi

[Coq-Club] Coq 8.6 is out!, Maxime Dénès, 12/16/2016
- Re: [Coq-Club] Coq 8.6 is out!, Ralf Jung, 12/16/2016
  - Re: [Coq-Club] Coq 8.6 is out!, Jeehoon Kang, 12/20/2016
    - Re: [Coq-Club] Coq 8.6 is out!, Benoît Viguier, 12/20/2016
      - Re: [Coq-Club] Coq 8.6 is out!, Ralf Jung, 12/20/2016
        
        Re: [Coq-Club] Coq 8.6 is out!, immanuel litzroth, 12/20/2016
        
        Re: [Coq-Club] Coq 8.6 is out!, Enrico Tassi, 12/21/2016
  - Re: [Coq-Club] Coq 8.6 is out!, Maxime Dénès, 12/20/2016
    - Re: [Coq-Club] Coq 8.6 is out!, Benoît Viguier, 12/21/2016