What is a hammer/atp within the logic of coq that does things like induction in coq?

just saw this: Inductive proof automation