Okay, it looks like I forgot to add the word “Coq” in the title… hence the name is pretty confusing. Could any admin change the title to “Primitive integers have been merged into Coq master”?
Sorry about that.
Yeah, without “Coq” in there you’re about 14 billion years late. ;)