The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

On Mon, Nov 21, 2011 at 11:35 PM, Michael Shulman 
<mshulman AT ucsd.edu>
 wrote:
> Here the argument A is maximally inserted to idmap.  So if "apply
> idmap" is immediately converted to "apply (@idmap _)", then how can
> Coq determine that the _ there should be A before it passes the term
> off to 'apply'?

Well, "apply (@idmap _)" works too, so I guess my incomprehension does
not come from maximally inserted implicit arguments. But I still don't
know why it works :-\ I'll let someone more familiar with the
internals of coq replies, sorry!
Alexandre