The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Dec 11, 2015 at 05:07:49PM -0500, Abhishek Anand wrote:
> *Is there a way to get both the brevity enabled by section variables, and*
> *the significant productivity-boost enabled by asynchronous proof
> checking? *

Somewhat ;-)

You can annotate your proofs with the set of section variables
actually used by starting them with "Proof using ...".  Such command
understands a little language designed to express a set of section
variables in a concise way. Also, if your section is very crowded, you
can use "Collection ..." to name a group of section variables you often
need to spell out.
Finally "Set Suggest Proof Using" and "Set Default Proof Using ..." may
come handy.

Everything should be documented in the reference manual, and there
should be pointers to all that in the chapter about asynchronous
proofs.  If not, please open a bug.

Ciao
-- 
Enrico Tassi