The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Thursday 31 July 2008 00:41:53 Brian Aydemir wrote:
> To expand on Andrew's remark, p and q in prop_eq are inferred to have
> type Type.  Thus, the eq argument to prop_eq is at Type, not at Prop.
>
> As a general remark: Enabling the printing of implicit arguments is a
> good way to debug problems where Coq refuses to match or unify terms
> that look identical to the user.
>
> -Brian

I suppose these kinds of error messages could be improved by having Coq check 
if the current string representation of each type is the same and, if so, 
display the types without implicit arguments.

Regards,

Sean