They have not been solved. My point was that automation via Coq's tactic language can serve as a decent substitute for "push-button" automation like Hammers, at least if one's continually working in the same domain and so can build up a library of tactics.