The Coq mailing list

[Vincent <vincent.siles AT gmail.com>]

Same here, I think we sent our messages almost at the same time :)
Sorry for the noise !
V.

2014-06-26 12:22 GMT+02:00 Marcus Ramos 
<marcus.ramos AT univasf.edu.br>:
> Hi Vincent,
>
> That was me, thanks for forwarding the question. As I had not seen your
> message before, I made another post with the same contents a few minutes
> ago. Sorry for the duplicate.
>
> Marcus.
>
>
> 2014-06-26 12:00 GMT+02:00 Vincent Siles 
> <vincent.siles AT ens-lyon.org>:
>
>> Hi club,
>> an interesting question was asked on StackOverflow yesterday, and I
>> have to say I don't understand why this simple apply fails. Consider
>> the script:
>>
>> Parameter P: nat -> Prop.
>> Parameter Q: nat -> Prop.
>> Hypothesis x : forall i, P i -> (forall k, Q k).
>>
>> Lemma y:
>>   forall i, P i -> (* Whatever *) P i.
>> Proof.
>>   intros i hPi.
>>   apply x in hPi.
>>
>> It fails with: Error: Unable to find an instance for the variable k.
>>
>> Why does Coq asks for the instantiation of k ?
>>
>> Best,
>> V.
>
>