The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/25/2014 04:51 PM, Jason Gross wrote:
> [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

Thanks, Jason.  I wanted implicit and maximally inserted - so Context 
{foo : bar} works.

> 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