The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/18/2014 04:17 PM, Christopher Ernest Sally wrote:
> Hmm, sorry for a horrible follow-up-email-style question, but what does
> maximally inserted mean?

This is about whether the function should behave in a curried fashion or 
non-curried fashion when the next argument is implicit. In practice, it 
controls when the subgoal to fill in that argument is generated.

From the reference manual, section 2.7.2:

"In case a function is partially applied, and the next argument to be 
applied is an implicit argument, two
disciplines are applicable. In the first case, the function is 
considered to have no arguments furtherly: one
says that the implicit argument is not maximally inserted. In the second 
case, the function is considered
to be implicitly applied to the implicit arguments it is waiting for: 
one says that the implicit argument is
maximally inserted."

Personally, I have yet to master all of the choices one has available 
about when and where implicit arg subgoals form, using things like 
refine vs. eapply vs. @-forms vs. "_" vs. Argument declarations vs. 
shelve_unifiable vs. unknown unknowns.  I realize it might be important 
with regards to my nemesis - evars - but I have other fish to fry first.

-- Jonathan