The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I would like to know if there is a way to register a hint in the typeclass database so that it gets called before [exact ...] for things added to the context.  For example:

Class A : Type := {}.

Axiom a : A.

Hint Extern 0 A => exact a : typeclass_instances.

Section bad.

  Variable b : A.

  Goal True.

  pose (_ : A).

  (* I want to see [a], not [b] *)

The reason I want to do this is to make it more pleasant to work around universe inconsistencies in a development version of Coq.

Perhaps I should submit a feature request to allow negative hint priorities?

Thanks,

Jason