The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 21 Mar 2011 11:16:13 +0100,
Hendrik Tews 
<tews AT os.inf.tu-dresden.de>
 a écrit :

> 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

AFAIK, there is no way now for such things, but you may be interested
by these things:

* You can use a good indentation
* You can go to this page: http://prover.cs.ru.nl/index.html
  and try proof web, and play with the "display" tab.
* I do not know if pcoq had something like this (but eitherway, it is
  dead now), I also heard of some similar things, but don't recall
  their names (and I believe, that they are dead too).
* Matita may have also good features for that and is very near
  coq. http://matita.cs.unibo.it/