The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2015 11:48 AM, Jason Gross wrote:
> A built-in [any] tactical lets you easily build [gprogress] (and many
> others) in ltac, while otherwise a dedicated [gprogress]-like tactic
> written in ocaml is needed for each tactic you want to have a global
> version of.

A case other than for use with [progress] where an [any] tactical would 
be useful is for solver tactics that fail if they don't solve the goal.  
Such as: [any omega] - as that would tell you if omega succeeded in any 
focused goal or failed in all.

-- Jonathan