The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 08/04/2015 10:52 AM, Enrico Tassi wrote:
> (...) Not putting the file in a flat format for performance reasons is
> debatable: when both the enclosed and enclosing lemmas are top level and
> complete , Coq is able to process their proofs asynchronously, so you don't
> have to wait much (this is what happens if you refactor the script when you
> see the warning).

I think you mean CoqIDE here, not Coq; if I understand correctly, the 
protocol that allows it to do that is still undocumented, and other common 
editors (mostly Proof General) do not have such capabilities.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature