Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness of existing Coq proofs.
Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness of existing Coq proofs.