The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/27/2014 04:33 PM, AUGER Cédric wrote:
> What would be nice with Coq reporting error is the following behavior: 
> if there is a subterm which is printed exactly like the one reported 
> in the error, then reprint the hypothesis and the error with display 
> of implicit arguments. For rewrite it may be not completely obvious on 
> how to do it, but for the error "xxx has type yyy while it is expected 
> to have type yyy", there temporarily automatically set display of 
> implicit arguments could be helpful (and probably reduce the number of 
> questions of this type on the Coq list). 

That would be an excellent addition.  By the time a newbie asks a 
question like this on the list, they've already probably experience a 
considerable amount of frustration.  Having error messages that don't 
scare away the uninitiated is an all-too-commonly overlooked feature in 
most software systems.

-- Jonathan