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
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
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.

Reply via email to