When I experiment, I get inconsistent results. Running the following code (with a proof included to double-check that it's provable)
Require Import Classical. Goal forall P, ~~P -> P. Proof. tauto. Qed. Goal forall P, P \/ ~P. Proof. exact classic. Qed. Goal forall P, P \/ ~P. Proof. tauto.
produces the error (on the last goal)
Tactic failure: Classical tauto failed.
which given the name "classical tauto" makes it sound like it's using classical logic, and it couldn't have proved the first goal without classical logic, so what's going on?
I tried looking at the tauto code but it's beyond my current level of understanding.