The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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.
> >