The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

What is the appropriate solution when Coq chooses the wrong maximally inserted
arguments? I have a lemma (generated by Brian's LNgen tool)

  binds_unique :
  forall (A key : Type) (x : key) (a b : A) (E : list (key * A))
    (Eqdec : EqDec key eq) (Fset : FSet key Eqdec),
  binds x a E -> binds x b E -> uniq E -> a = b
  
  No implicit arguments

Although no arguments are implicit, some are 'maximally inserted' (I think); 
in
particular, when I do

  eapply binds_unique.

Then it seems to pick whatever instantiation of 'A key x..' it can find (the
wrong one, as it happens). When I do

  eapply binds_unique with (key := atom).

things work out; since I want this to happen automatically, I can do

  Hint Extern 2 ( _= _) => eapply binds_unique with (key := atom).

but it is slightly annoying that Coq picks the wrong argument without even
telling me that it is picking any.

Now, how can I find out which arguments are 'maximally inserted', and does 
one usually solve problems such as these? Is my workaround paradigmatic?

Thanks,

Edsko