This bug only effects proofs that use types with more than 256 constructors. Also, it involves a command that is meant to optimize proofs so it isn't neccessary to ever use it. Personally, I still trust the implementation despite this edge case.
I believe this comment is meant to be a response to another post (https://news.ycombinator.com/item?id=18155410) who pointed out a flaw (now fixed) in Coq that allowed false theorems to be proved.
Github link: