The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Maybe I'm getting old but you seem to solve only one goal here, for x1 don't you? In the previous engine, dependent "holes" were kept as existentials, independent became metas that became goals. 

Le mardi 7 janvier 2014, Beta Ziliani  a écrit :
> On Tue, Jan 7, 2014 at 10:04 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:
>
> > That's not doable in 8.4 but is in trunk thanks to Arnaud Spiwack's new
> > proof engine. Long story short, the previous proof engine used an ad-hoc
> > tree with leaves representing the subgoals, instead of using directly the
> > term tree structure + holes/existentials.
>
> Then I'm curious to know why refine does the job in 8.4:
>
> "
> Inductive I := Iconstr :  forall ( x0 : Type ) ( x1 : x0 ) , I .
>
> Goal I.
> refine (Iconstr _ _).
> refine 0.
> Qed.
> "
>
>
>
> >
> > Le mardi 7 janvier 2014, Vladimir Voevodsky a écrit :
> >
> >> Is there a reason why Coq's proof engine does not accept a possibility of
> >> dependent goals? For example if I need to provide an object of an inductive
> >> type
> >>
> >> Inductive I := Iconstr :  forall ( x0 : T0 ) ( x1 : T1 ) , I .
> >>
> >> where T1 in general depends on x0, I would like to say "apply Iconstr."
> >> and get provided first with the goal to fill in x0 in T0 and then with the
> >> goal to fill in x1 in the appropriately substituted T1.
> >>
> >> This should not be too hard to implement and it would make many proofs
> >> easier.
> >>
> >> Vladimir.
> >
> >
> >
> > --
> > -- Matthieu


-- 
-- Matthieu