The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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. 

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