coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Info about error message

From: Vincent Aravantinos <vincent.aravantinos AT yahoo.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Info about error message
Date: Thu, 24 Jan 2008 21:30:03 +0100
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Received:X-YMail-OSG:X-Yahoo-Newman-Property:Mime-Version:Content-Transfer-Encoding:Message-Id:Content-Type:To:From:Subject:Date:X-Mailer; b=XJCsmN7NAksm3xG4Ceh3+HvUCFLQFkPiu2qGqjfutFaarH/Ir29Ih3pPoY4Sl1YcDbS60fR+PA5wFyI0Ls7EAfamvQkRJZqM5lSoTNyor/6gUTKFGqUyZMKIfVMBFUA5rdNahfx5VHz/6TN4NndjF3jao8QhRgQlbX6ivldomP4= ;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

[Coq-Club] Info about error message, Vincent Aravantinos
- <Possible follow-ups>
- [Coq-Club] Info about error message, Vincent Aravantinos
  - Re: [Coq-Club] Info about error message, Andrew McCreight