The Coq mailing list

[Greg Morrisett <morrisett AT gmail.com>]

It's very likely that the implicit arguments aren't the same.  For instance, that (inl n) would be (@inl A n) when what's needed is an (@inl B n).  Using the "Set Printing All." directive will allow you to determine what's different.

-Greg

On Mon, Jun 29, 2015 at 10:31 AM, Marcus Ramos <marcus.ramos AT univasf.edu.br> wrote:

Hi,

What should I do when I get the following error message?

"The term "H29" has type "In (inl n) (map inl r')"

 while it is expected to have type "In (inl n) (map inl r')"."

I am using Coq 8.4 pl14 in CoqIDE for Windows 8.

Thanks in advance,

Marcus.