The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

Besides the Coq manual, other good sources of Coq documentation are the 
FAQ and Cocorico!, which are linked from the documentation page.  I don't 
know that they will help with your particular problem. Also, using Google 
can sometimes find something, although searching for your particular error 
only seems to turn up the commit message that added this error [1]. 
Maybe that will sort of help?

Another thing you can do is to file a bug report requesting that this 
particular error be documented.  I've reported things missing from the 
documentation before, and they've been added.  While this doesn't really 
help you immediately, it will hopefully help to improve things for others 
in the future.

-Andrew

[1] 
http://lists.gforge.inria.fr/pipermail/coq-commits/2007-April/001187.html


On Thu, 24 Jan 2008, Vincent Aravantinos wrote:

> Hi,
>
> I'm encountering the following error while doing an "apply ... in" :
>
> "User error: cannot find an instance for ... "
>
> And I can't find any documentation about this error so I don't really know 
> how to interpret it.
> I have the feeling it's a 2nd order unification pb but I am not quite sure.
> Is there a kind of hidden doc that would document things that are not in the 
> user manual ?
>
> (Please notice I didn't ask for how to solve my error but just for some doc 
> about it, I'd like to do it by myself :).
>
> Thanks !
> V.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>        http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club