The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[Context {foo : bar}.] will mark mark [foo] as implicit and maximally inserted.  [Set Implicit Arguments.] will make inferrable variables automatically implicit (but not maximally inserted).  I don't know if there's a way to explicitly mark variables as implicit but not maximally inserted, or to get automatic implicit-and-maximally-inserted variables.

-Jason

On Fri, Apr 25, 2014 at 4:47 PM, Jonathan <jonikelee AT gmail.com> wrote:

Is there a way concise to mark certain variables declared in a section as implicit?  Or, does one have to use a separate Arguments command for each function declared in that section?

-- Jonathan