An attribute marking a tactic unit or tactic string which should be used by the hint
add_hint_tactic t runs the tactic t whenever hint is invoked.
The typical use case is add_hint_tactic "foo" for some interactive tactic foo.
Report a list of tactics that can make progress against the current goal,
and for each such tactic, the number of remaining goals afterwards.
Report a list of tactics that can make progress against the current goal.