The Coq mailing list

[Andrew Kent <sgtamk AT gmail.com>]

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