The Coq mailing list

[Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>]

  Hello,

I have a question regarding saving proofs in Coq, namely, how to do it. 
That is, I would like to be able to do the following (in coqtop). 
1. State some lemma.
2. Prove it (using coqtop).
3. Somehow save the proof (and lemma) so that next time I can proceed with 
the development with the lemma proved. 

What I've been doing so far was stating the lemmas in the .v file, and 
simply pasting proofs to this file; this methodology, though, stopped 
being sufficient once proofs got large. The Write State command, which 
from the description could be what I'm looking for, doesn't seem to be 
working. 

Thanks,

Wojtek