The Coq mailing list

[marko AT ffri.hr]

I'm sorry; the term "managing memory" is uncouthly for what I need. I need
it from high Coq's point of view. In system I develop I have all the time
lot of (un)prooved subgoals. Proved subgoals are not interesting for me
but unproved are. I guess the Coq keep all of them in RAM until I proving
the main goal. Is it correct? I need to optimize the time of processing.
Is it possible to store unproved subgoals on hard disk and then erase them
from memory? Later I will take it from disk as needed. I found just "Write
state" command but it does not help me.

Thank you very much,

Marko Malikoviæ