The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 9 mars 2012 à 16:22, Gregory Bush a écrit :

> 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?

Hi Gregory,

  you can use [Hint Resolve (@ex)] for adding the parametric hint.
-- Matthieu