The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/20/2014 11:01 AM, Andrew Kent wrote:
> Greetings all,
>
> I was just curious if there was a nice, neat way to try automatically solving 
> all the goals generated from “Grab Existential Variables”.
>
> It would be nice if, for example, there was something I could write like 
> “Grab Existential Variables; auto.” (this, btw, is a syntax error) instead of 
> writing “Grab Existential Variables; auto. auto. auto.” For a moment I 
> thought “Solve All Obligations using auto.” might work, but it looks like 
> these are not considered “obligations” by Coq.
>
> Best,
> Andrew

In the trunk version, you can do:  "Grab Existential Variables. all:auto."

-- Jonathan