That is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the

That is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the start? As far as I'm aware, the question of moving the "sledgehammer" approach to a constructive setting is still an open problem.