prooftree - proof-tree visualization for Proof General

Property Value
Distribution Ubuntu 18.04 LTS (Bionic Beaver)
Repository Ubuntu Universe i386
Package filename prooftree_0.13-1build3_i386.deb
Package name prooftree
Package version 0.13
Package release 1build3
Package architecture i386
Package type deb
Category universe/science
License -
Maintainer Ubuntu Developers <>
Download size 732.50 KB
Installed size 3.35 MB
Prooftree draws proof trees during interactive proof development
with Proof General. One can inspect goals and proof commands
and check where existential variables were introduced and
instantiated. Currently, Prooftree does only work for Coq.


Package Version Architecture Repository
prooftree_0.13-1build3_amd64.deb 0.13 amd64 Ubuntu Universe
prooftree - - -


Name Value
coq >= 8.4
libc6 >= 2.17
libgdk-pixbuf2.0-0 >= 2.22.0
libglib2.0-0 >= 2.35.9
libgtk2.0-0 >= 2.24.31
libpango-1.0-0 >= 1.14.0
proofgeneral >= 4.3~pre130510


Type URL
Binary Package prooftree_0.13-1build3_i386.deb
Source Package prooftree

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install prooftree deb package:
    # sudo apt-get install prooftree




2017-10-28 - Gianfranco Costamagna <>
prooftree (0.13-1build3) bionic; urgency=medium
* Rebuild against new OCAML ABIs.
2017-07-27 - Dimitri John Ledkov <>
prooftree (0.13-1build2) artful; urgency=high
* No change rebuild against new findlib.
2017-06-30 - Dimitri John Ledkov <>
prooftree (0.13-1build1) artful; urgency=high
* No change rebuild against ocaml 4.04.
2017-01-03 - Hendrik Tews <>
prooftree (0.13-1) unstable; urgency=medium
* Imported Upstream version 0.13
* delete patch 0001-Fix-compilation-with-OCaml-4.02 (problem fixed upstream)
* push standards version to 3.9.8
* fix some lintian warnings
2015-10-14 - St├ęphane Glondu <>
prooftree (0.12-2) unstable; urgency=low
[ St├ęphane Glondu ]
* Team upload
* Fix compilation with OCaml 4.02
[ Hendrik Tews ]
* lintian canonical vcs
2013-05-17 - Hendrik Tews <>
prooftree (0.12-1) unstable; urgency=low
* Initial release (Closes: #672480)

See Also

Package Description
proot_5.1.0-1.2_i386.deb emulate chroot, bind mount and binfmt_misc for non-root users
propaganda-debian_13.5.10_all.deb Propaganda background image volume for Debian
propellor_5.3.3-1_i386.deb property-based host configuration management in haskell
prosody-modules_0.0~hg20170929.c53cc1ae4788+dfsg-3_all.deb Selection of community modules for Prosody
prosody_0.10.0-1build1_i386.deb Lightweight Jabber/XMPP server
prosper_2017.20180305-1_all.deb TeX Live: transitional dummy package
proteinortho_5.16+dfsg-1_i386.deb Detection of (Co-)orthologs in large-scale protein analysis
protobuf-c-compiler_1.2.1-2_i386.deb Protocol Buffers C compiler (protobuf-c)
protobuf-compiler-grpc_1.3.2-1.1~build1_i386.deb high performance general RPC framework - protobuf plugin
protobuf-compiler_3.0.0-9.1ubuntu1_i386.deb compiler for protocol buffer definition files
protracker_2.3d.r92-1_i386.deb Amiga ProTracker v2.3D clone for modern computers
prottest_3.4.2+dfsg-2_all.deb selection of best-fit models of protein evolution
prov-tools_1.5.0-2_all.deb tools for prov
prover9-doc_0.0.200902a-2_all.deb documentation for Prover9 and associated programs
prover9-mace4_0.5.dfsg-3_all.deb GUI for Prover9 and Mace4