The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.