The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/18/2014 04:03 PM, Christopher Ernest Sally wrote:
> Hi all
>
> I have a Section where I declare Variable foo : Type, and after I close the
> Section, of course all my functions inside the section will have forall
> foo: Type, etcetcetc.
>
> My question is: Is there a neat way to get foo to be implicit? I only know
> how to do it the usual way, but I have 30+ plus functions in the section...
> and so wouldn't like a whole bunch of
> Implicit Arguments fun1 [foo].
> Implicit Arguments fun2 [foo].
>
> Thanks
>
> Warm regards
> Chris

I asked the very same question a few weeks ago...

"Context {foo : Type}." does the trick.

-- Jonathan