The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

But it now is, in the v8.5 branch of Coq.

Le mercredi 25 mars 2015, Laurent Théry <Laurent.Thery AT inria.fr> a écrit :
> Unfortunately you increase your trusted base when using vm_compute.
> In this case, you hit one of the limitation of the byte-code machinery. It is just a pity
> it was not checked by the command.
>
>
>
> On 03/25/2015 06:30 PM, Jonathan Leivent wrote:
> > On 03/25/2015 12:55 PM, Laurent Théry wrote:
> > > > OK - I'm panicking a bit less...
> > >
> > > Were you  using an inductive type with more than 255 constructors? ;-)
> >
> > I didn't say what "a bit less" was relative to ;-)
> >
> >
> > Still, I was under the ever-so-slightly? mistaken impression that things are either outside (and hence checked by) the kernel, or, if in the kernel, are simple enough and scrutinized enough not to encounter such issues.
> >
> > -- Jonathan


--