The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/29/2015 10:43 AM, Pierre Courtieu wrote:
> 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

Is there also a very common corresponding enhancement request: why not 
have Coq determine whether the two types will be visibly different when 
printed under the current settings - and if not, temporarily Set 
Printing All (and say that it is doing so to avoid confusion) in order 
to display a more meaningful error message - perhaps after first 
printing the type under current settings so that the user would have an 
easier time following the correspondence?

-- Jonathan

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