The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Quick answer (very common question). Try replaying the error after setting this: "Set Printing All."

This will disable the hiding of implicit arguments and notations that make you believe these two types are the same.

Best regards,

Pierre

2015-06-29 16:31 GMT+02: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.