Looks impressive! I agree, use a branch for now until we can release PG 4.1
and then merge back in.
On 13 Apr 2011, at 08:29, Hendrik Tews wrote:
> 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''?
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.