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

<<inline: window.png>>

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to