The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/24/2015 02:43 AM, Jason Gross wrote:
> Hi,
>
> In trunk/8.5, is there a tactical that means "progresses in at least one
> goal"?  I tried `progress [> intros ]`, but this fails if any of the goals
> has no hypotheses to introduce, and I want it to fail only if all of the
> goals have no hypotheses to introduce.
>
> Thanks,
> Jason

I learned recently from Arnaud, by way of bug 3878, that attempting to 
keep a global focus in tactic expressions is very difficult. None of the 
tacticals - progress, once, try, etc.. - will keep a global focus.  
Hence 'progress [> intros ..]' is equivalent to '[> progress intros..]'.

-- Jonathan