The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I think that "apply … with (B := …)" also works.

2014-06-17 13:44 GMT+02:00 Greg Morrisett <greg AT eecs.harvard.edu>:

Use something like:

  apply (@inl foo bar)

or

  apply (@inl(B:=bar))

where the goal is something of type foo+bar.

-Greg

On 6/17/2014 7:38 AM, Marcus Ramos wrote:

Hi,

I get the error message "Cannot infer the implicit parameter B of inl."
​ when using apply.. with...​
How do I fix it?

Thanks,
Marcus.

--
.../Sedrikov\...