The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/24/2014 10:28 AM, Arnaud Spiwack wrote:
> Try this in trunk. It will hopefully explain better than words:
>
> Goal exists n, n=0.
> Proof.
>    refine (ex_intro _ _ _).
>
> Currently the only way to introduce dependent subgoal is to use the
> [refine] tactic.

I still don't get it.  If I use "eexists" instead of that refine, I get 
only the second subgoal that refine produces, not the first. How is 
being forced to solve two subgoals better than one?

Maybe exists/ex_intro is a poor example - but wouldn't econstructor work 
in the general case?

-- Jonathan

> On 24 July 2014 15:05, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > On 07/24/2014 05:27 AM, Arnaud Spiwack wrote:
> >
> > > ... the new dependent subgoal feature
> > What is the new dependent subgoal feature?
> >
> > -- Jonathan