The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Dear Adam, Dear All,
  This seems to be an interesting question. Perhaps it rather points to a need for a mechanism for
recording a trace of Ltac calculations in an external file, which could be reloaded at subsequent passages
of that point in the proof process. In that case, when you arrive at a point where a long Ltac calculation
has been made, but realize you need a lemma, you could save the Ltac trace (which should be available
during the current proof script); back up, put the lemma in before, and then recover up to the
place where the lemma is to be used by having Ltac use its saved trace as a big "hint". This type of
capability would certainly be useful elsewhere, not to speak of what happens the next day when you
try to rerun the proof.
All the best,
---Carlos Simpson

Le 04/08/2015 16:36, Adam Chlipala a écrit :

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.