The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Adam Chlipala wrote:
> fdabrows AT irisa.fr
>  wrote:
> > > Hello,
> > >
> > > I am fairly new to Coq and I am not sure if this is the right place to
> > >     
> > ask but I am hoping someone can help me. I am having trouble with what I
> > think should be a simple proof. I am trying to solve the following
> >  
> > > forall x, P x^Q x |- (forall x Px) ^(forall x Qx)
> > >     
>
> 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. ;-)
It is new in Coq version 8.2, isn't it?

--
Best regards,
 Roman Beslik.