The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Thomas Braibant wrote:
> > > I feel like I should jump in and bring up that the built-in [firstorder]
> > > tactic solves this goal, so that's the right way to do it in real
> > > developments. ;-)
> > >       
>
> At this point, I fell I should ask what are the relative
> advantages/disadvantages of using intuition versus firstorder in a
> real development ? The manual is not very clear about this.
>   

[firstorder] may run into an infinite loop, even without an infinite 
loop in the tactic you pass to it to discharge remaining subgoals.  
Because of this, I only try [firstorder] when [intuition] fails (and it 
seems like something generic should do the job), and I give up if 
[firstorder] runs for more than a few seconds without finishing.