coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Samuel Bronson" <naesten AT gmail.com>
- To: "Sean Wilson" <sean.wilson AT ed.ac.uk>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Coq doesn't match identic types?
- Date: Thu, 31 Jul 2008 09:50:08 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=ECBkwGdFDwUgld9Dkh4WANAIXygNdDo3blPUGRGoWYCzkZ4UbZ6wbbCxetl7npX5Q1 Ag9vupiJYWxhuQXe+O14smi4pJbkVuvWraDnzKIq8BoW5+vofuMXe1h8tlzc9YoLEDGG OUp8hWqfbwg67mHNHakZRHIJ2REyLFCi9tyrc=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On 7/30/08, Sean Wilson
<sean.wilson AT ed.ac.uk>
wrote:
> 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.
I would be more interested in having it explain why the unification
failed -- often when I see this type of error, the two types have
functions at their heads, and it would be nice to see what they
expanded to before unification failed.
- [Coq-Club] Coq doesn't match identic types?, see tolearn
- Re: [Coq-Club] Coq doesn't match identic types?,
Andrew McCreight
- Re: [Coq-Club] Coq doesn't match identic types?,
Brian Aydemir
- Re: [Coq-Club] Coq doesn't match identic types?,
Sean Wilson
- Re: [Coq-Club] Coq doesn't match identic types?, Samuel Bronson
- Re: [Coq-Club] Coq doesn't match identic types?,
Sean Wilson
- Re: [Coq-Club] Coq doesn't match identic types?,
Brian Aydemir
- Re: [Coq-Club] Coq doesn't match identic types?, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] Coq doesn't match identic types?,
rabforum
- Re: [Coq-Club] Coq doesn't match identic types?, Adam Chlipala
- Re: [Coq-Club] Coq doesn't match identic types?,
Andrew McCreight
Archive powered by MhonArc 2.6.16.