coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Difference between external hints and non-external hints for typeclass resolution?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Difference between external hints and non-external hints for typeclass resolution?
Date: Thu, 5 Jun 2014 17:07:09 +0100

Hi,

I am wondering what the difference is between [Hint Extern] and [Instance] is for typeclasses? When I switch from instances to [Hint Extern], typeclass resolution goes from being instantaneous to taking around 1.3 seconds. I'll work on minimizing it, but I'm curious if anyone knows why this might be.

-Jason

[Coq-Club] Difference between external hints and non-external hints for typeclass resolution?, Jason Gross, 06/05/2014