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:
Even coq have had its bugs where it was possible to prove that true is false: https://github.com/clarus/falso
Is the Coq bug you're thinking of this one, from earlier this year?