The following commit has been merged in the master branch:
commit 71b6c241a5b56a8245efbcc6fca83530e2df36c4
Author: Hendrik Tews <>
Date:   Tue May 15 11:04:23 2012 +0200


diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..b25c15b
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
diff --git a/debian/README.Debian b/debian/README.Debian
new file mode 100644
index 0000000..1437f06
--- /dev/null
+++ b/debian/README.Debian
@@ -0,0 +1,25 @@
+Prooftree: proof-tree visualization for Proof General
+Prooftree does only work for Coq version 8.4beta or later. Currently
+you need to install Coq 8.4beta manually or by fetching packages from
+experimental. Once you have done this, you have to enable the
+prooftree support in Proof General by setting `proof-tree-configured'
+to t (either do M-x customize-variable proof-tree-configured or
+include (setq proof-tree-configured t) in your .emacs).
+Background: To properly work, prooftree needs support form the proof
+assistant and from Proof General. Generic and Coq specific support is
+included in the 4.2 prereleases of Proof General and thus present in
+Debian Wheezy. In Coq, prooftree support has been included in the
+development version before the 8.4beta release. It is therefore only
+included in 8.4beta or later versions. Because there has been no
+proper 8.4 release of Coq until now, prooftree support in Coq is
+currently missing in Debian Wheezy.
+There is work underway to get prooftree working for HOL Light.
+However, the current state is too preliminary to get included in
+ -- Hendrik Tews <>, Tue, 15 May 2012 10:57:15 +0200

prooftree packaging

Pkg-ocaml-maint-commits mailing list

Reply via email to