The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2015 03:38 AM, Arnaud Spiwack wrote:
> Just as a note: progress is a bit of a complex tactic, contrary to the
> tryif, (||), repeat, etc… it may require some work to make a "global"
> version. I'll try and think about it when v8.5 is released, though you may
> want to remind me then, because, honestly, I don't like spending time in
> the relevant code and my mind may just forget to prevent me from the
> headaches.

I'd rather have a built-in any tactical than a global progress tactical.

-- Jonathan