The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

Let's say I have some type class that contains proofs of some  
propositions...

Variable ExProp : Prop.

Class ExClass := {
  ex : ExProp
  (* ... *)
}.

I'd like to add "ex" and friends to a hint database, but

Hint Resolve ex.

fails since it doesn't have an instance of ExClass in scope.

I can prove an ex' : forall (C : ExClass), ExProp, then add ex' to a  
hint database, but it's kind of tedious.

Is there a nicer way to do this?