Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Expose a Obj.last_variant_tag constant #6834
Original bug ID: 6834
It would be nice to advertise the value of the last-usable-tag (for non-constant constructors). Currently people just assume it is Obj.lazy_tag - 1, but this limit is not currently specified anywhere.
This was prompted by Benjamin Grégoire changes in the vm_compute mechanism of Coq, after Maxime Dénès remarked the lack of check for out-of-bound tags.