[Apologies if you've already seen this message on Coq-Club.]
In Proof General, do you use the Show/Hide context menu? If so, do you
use it to hide individual items, like tactic calls, or Notation
declarations, or do you use to hide chunks, like proofs and sections?
I'm working on a new version of Proof General, and I can get some
speedup if I can avoid creating some of those context menus, so I'd
like to get some sense of how this feature is used.
ProofGeneral mailing list