The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  sadly, that was overlooked in 8.4, it is available in the trunk though.
Interestingly [Hint Resolve foo 4 : typeclass_instances] could have been
a workaround, as the grammar can expect an int at the end of the list of 
hints, but 4 parses as a term… I'm changing the syntax to: 
[Hint Resolve hint [| n] : …], avoiding ambiguity and maintaining 
compatibility. For now, the only workaround is to use:
[Hint Extern 4 (optional pattern) => apply hint : typeclass_instances].

Best,
-- Matthieu

On 6 sept. 2013, at 16:50, Thomas Braibant 
<thomas.braibant AT gmail.com>
 wrote:

> Hi list,
> 
> The documentation states that
> Instance ident binder1 …bindern : Class t1 …tn [| priority] := {
> field1 := b1 ; …; fieldi := bi }
> defines an instance with a priority.
> 
> I cannot remember (if I ever knew it) what is the relevant syntax to
> add priorities to instances defined using Existing Instance?
> 
> With best regards,
> Thomas