Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page