Guillaume Melquiond

Thanks for pointing out the existence of that project; I was not aware of it. It seems that other project predates this one by a few months. The confusion is...

I think your example is a bit off. A .cmo file does not depend on the presence of a .mli file, it depends on its absence. Currently, if a .cmo...

Please let us not replace a trivial opcode with a costly memory-allocating one. That said, having an additional opcode of type `forall x y:int, option (x = y)` makes sense...

> The reduction could be provided by going through a sprop equality (using the uip flag). That is elegant. But wouldn't that still block due to the use of `vm_compute`...

> it only chooses one equality proof, `eq_refl`, but doesn't prevent the existence of other equality proofs on `int` Just to be clear, there is no other equality proof. And...

Actually, I meant your point 1. At the time of retro-knowledge, `int` had a concrete definition, and thus UIP was provable. And nowadays, even if the type has become abstract,...

>> Please let us not replace a trivial opcode with a costly memory-allocating one. > One option would be to actually replace the current primitive `eqb` with an operator `eq_option`...

> It's safer to write code in lambda than in C... I dispute this statement. When I had to debug a memory corruption due to cofixpoints in the VM, I...

> there is a clear program that does what we want, which is the Gallina equivalent of the lambda program above. This is exactly what I was about to write....

> This PR relicenses the implementation of primitive ints, floats, and arrays, from LGPL-2.1-only to MIT. I do not agree to the relicensing of my code to a MIT license.