coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] I am completely befuddled by this error message.

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] I am completely befuddled by this error message.
Date: Wed, 24 Jun 2009 22:18:59 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=OJgbbiw8rTQ7B3C/NVv2hZ3dHHGvlWeeOms0u/CSynJhgbUyt3ba/7NVqYfqrRSa/n 3eTt19z58WOYEcDrrVSqkydN/PnATNsWeuz4ALdXVTd7j4QemUJI4czxASwtXFMOQjoG TgbRvPohAC06SIw3F1fsarjQgNEkYsw4dBuOA=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

The term "H4" has type "refs' = refs" while it is expected to have type
"refs' = refs"

� Funny as it seems, this can happen. My bet would be on difference in implicit arguments. Try:
� Set Printing Implicit.
� and see whether the error message is more informative then.

� Cheers,
�� Adam

--
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[Coq-Club] I am completely befuddled by this error message., M. Scott Doerrie
- Re: [Coq-Club] I am completely befuddled by this error message., Brian Aydemir
- Re: [Coq-Club] I am completely befuddled by this error message., Adam Chlipala
- Re: [Coq-Club] I am completely befuddled by this error message., Adam Koprowski