coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Stoughton, Alley - 0558 - MITLL" <Alley.Stoughton AT ll.mit.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] controlling undo history?
- Date: Sat, 26 Jan 2013 10:45:00 -0500
- Accept-language: en-US
- Acceptlanguage: en-US
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
- [Coq-Club] controlling undo history?, Stoughton, Alley - 0558 - MITLL, 01/26/2013
Archive powered by MHonArc 2.6.18.