The Coq mailing list

[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.