AFAIK the four color theorem was not first proved with Coq, and people consider it correct regardless of whether Coq has bugs.
Yes, the four color theorem was proven by Appel and Haken on an IBM 370-168 at the University of Illinois in June 1976. Coq was released in May 1989.
I'd be surprised Appel and Haken did a formal proof on their machine -- I thought they made a conventional proof with a machine-assisted enumeration of special-cases.
My apologies for the lack of clarity: I was following the thought path that was concerned with the validity of the four color theorem proof because of the Coq bug.
It shouldn't, really. It'll only invalidate results that
a) rely on this bug, and
b) haven't been formally proven any other way.
It is a valid concern when talking about theorem provers, though.