The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks. It is indeed well documented here in the manual.

(I'm surprised that google never found the above page of the manual when I was searching about asynchronous proof checking in CoqIDE.

No matter what I search, even verbatim quoted sentences from the page, google cannot find the page.)

Sorry for the noise,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Dec 11, 2015 at 6:39 PM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

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