The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.

On 08/04/2015 10:04 AM, Cedric Auger wrote:

If so, I was wrong about how nested lemma work (I did not tried it). And almost all what I wrote could be forgotten.

I simply guessed that the mechanism was similar to what occurs with the "abstract" tactic.

But well, in that case, I could not find really relevant arguments to remove this feature (but even less to keep it, in fact, beside retrocompatibility).

Thus I will only state that it needlessly (from my point of view) complicates the syntax, and I find it simpler to keep the "Lemma L1 : … Qed. Lemma L2 : … Qed …" form, rather than having well parenthesized "Dyck" lemmas.

In my experience of Coq, I never needed that feature.