coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] evars, metas, and typeclass resolution

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] evars, metas, and typeclass resolution
Date: Tue, 9 Sep 2014 13:40:36 -0400

Is there a description somewhere of when in the typechecking/type inference process holes are turned into evars/metas (and what the difference is between these), and when typeclass resolution is run?

Thanks,

Jason

[Coq-Club] evars, metas, and typeclass resolution, Jason Gross, 09/09/2014