The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

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