Hi, inspired by PVS, I started to work on an external visualization of the proof tree. I have now a basic version running, see below. It is implemented in GTK and Ocaml, integrated with Proof General and works with a patched version of Coq.
I believe it's time now to share the code with others and I would therefore like to commit the necessary changes to the repository of Proof General. It probably makes sense to commit to a branch first. How about ``ProofTreeBranch''? Bye, Hendrik
_______________________________________________ ProofGeneral-devel mailing list ProofGeneralemail@example.com http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel