2013, Adam Chlipala,Certified Programming with Dependent Types:
Therepeat that we use here is called atactical, or tactic combinator. The behavior ofrepeatt is to loop through runningt, runningt on all generated subgoals, runningt ontheir generated subgoals, and so on. Whent fails at any point in this search tree, that particular subgoal is left to be handled by later tactics.