Major Section: PSTACK
By evaluating (verbose-pstack t) one can get trace-like information
during subsequent proofs about prover functions, including time summaries,
printed to the screen during a proof. To turn off this feature, evaluate
(verbose-pstack nil). Also See pstack.