I'm learning Coq and the book I'm learning from, (CPDT) makes heavy use of auto in proofs.

Since I'm learning I think it might be helpful for me to see exactly what auto is doing under the hood (the less magic early on the better). Is there any way to force it to display exactly what tactics or techniques it's using to compute the proof?

If not, is there a place which details exactly what auto does?

rocq-prover verbose
Edit
Report