The Coq mailing list

["Stoughton, Alley - 0558 - MITLL" <Alley.Stoughton AT ll.mit.edu>]

When proving some lemmas (generated by Why3 from EasyCrypt) with numerous
conjuncts in hypotheses and conclusions, I found that the deeper I got
into the proof, the slower coqtop became. Eventually, even simple tactics
(e.g., assumption) were taking over a minute to run.  But if I then
admitted the rest of the proof, and then reloaded into coqtop, everything
ran quickly again.

It's been suggested to me that this is an issue with the undo history
that's collected.  (I was doing lots of focusing and unfocusing.) But I
can't find a way of limiting this history in the manual or FAQ.  Is there
a command for doing this?  Or does anyone have another suggestion about
what's going on or how to rectify it?

Thanks!

Alley