coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] wrong inference of an implicit argument

From: Bas Spitters <spitters AT cs.ru.nl>
To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] wrong inference of an implicit argument
Date: Fri, 1 Jul 2011 09:13:48 +0200

Dear Matthieu,

On Fri, Jul 1, 2011 at 1:11 AM, Matthieu Sozeau
<matthieu.sozeau AT gmail.com>
wrote:
> It is however a different problem from making definitions polymorphic.
> I have a tentative patch for the later [1] (mainly the kernel/*.ml changes
> are necessary),
> and it seems not to cause any problem. It is also justified by Harper and
> Pollack's
> version of typical ambiguity with definitions.
>
> [1]
> https://github.com/mattam82/Coq-misc/commit/d98dfbcae463f8d699765e2d7004becd7714d6cf#diff-6

I have experimented with this, but I could not figure out what this
feature actually does.
I've put a precise HoTT test case in the bug tracker:

http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2298

Best,

Bas

Re: [Coq-Club] wrong inference of an implicit argument, Matthieu Sozeau
- Re: [Coq-Club] wrong inference of an implicit argument, Vladimir Voevodsky
  - Re: [Coq-Club] wrong inference of an implicit argument, Matthieu Sozeau
- Re: [Coq-Club] wrong inference of an implicit argument, Bas Spitters
- <Possible follow-ups>
- Re: [Coq-Club] wrong inference of an implicit argument, Georgi Guninski