The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello Théo. Why don't you announce the availability of a new version 
only when it is actually available on opam?

Le 09/10/2019 à 18:25, Théo Zimmermann a écrit :
> The opam package is actively being worked on:
> https://github.com/ocaml/opam-repository/pull/15017
>
> I don't participate, so I wouldn't be able to estimate accurately, but
> I'd say it shouldn't take long before the pull request is merged and
> the package is available.
>
> Cheers,
> Théo
>
> Le mer. 9 oct. 2019 à 18:24, Xuanrui Qi 
> <xuanrui AT cs.tufts.edu>
>  a écrit :
> > Hi,
> >
> > How long do we have to wait approximately for 8.10.0 to be on opam?
> >
> > Thanks,
> > Xuanrui
> >
> > On Wed, 2019-10-09 at 15:27 +0000, Vincent Laporte wrote:
> > > 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.