The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Just for the records: I used "Display implicit arguments" and was able to locate and correct the problem.

Best Regards,

Marcus.

2015-06-29 15:31 GMT+01:00 Marcus Ramos <marcus.ramos AT univasf.edu.br>:

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.