The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Hi,

from PVS I am used to a graphical visualization of the proof tree
(see http://askra.de/software/coq-tree/proof-tree.jpg for an
example). This is especially useful when you switch to the next
branch in a proof and you need to understand where the current
proof obligation comes from.

Does anybody know something similar for coq?

Bye,

Hendrik Tews