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.