coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq doesn't match identic types?

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?, 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