The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT inria.fr>]

Le 7 janv. 2014 à 21:51, Vladimir Voevodsky 
<vladimir AT ias.edu>
 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.
"eapply Iconstr" do no works ? 
> 
> Vladimir.