The Coq mailing list

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

On Tue, Aug 04, 2015 at 10:36:28AM -0400, Adam Chlipala wrote:
> Again, for highly automated proofs, it often makes a /huge/
> difference to save the need to rerun even one line of a proof
> script.  This feature facilitates that process optimization.

Hello, the warning was added because the current implementation/behavior
is a source of complexity. For example the global scope of a nested
lemma makes it impossible to process the enclosing proof asynchronously.

The new warning is generated when the enclosing proof is ended to still
let people state, and even prove, the nested lemma where/when its need
is felt, but then the user is asked to put the script in flat form, to
ease the re-processing of the document. 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). 

When the nested lemma is morally local but useful to many sub goals I
think assert is more clean, and some proof languages even have support
for bubbling-up sub proofs as much as needed with minimal edits.

On a side note, are nested lemmas documented?

best
-- 
Enrico Tassi