The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

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