Looks impressive! I agree, use a branch for now until we can release PG 4.1 and then merge back in.
- D. On 13 Apr 2011, at 08:29, Hendrik Tews wrote: > 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 > > <window.png>_______________________________________________ > ProofGeneral-devel mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
