New upstream release: 8.0pl2.debian/8.0pl2-1

1 files changed, 25 insertions, 11 deletions

diff --git a/debian/README.Debian b/debian/README.Debian
index 5657bfca..685f6047 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -1,5 +1,28 @@
-Coq package for Debian
-----------------------
+--------------------------
++ Coq package for Debian +
+--------------------------
+
+Binary (in)compatibility
+------------------------
+The compiled libraries of Coq (the *.vo) are not expected to be backward or
+upward compatible between releases (including plX releases). In case of a new
+upstream release, your Coq files should be recompiled.
+
+
+Coq frontends
+-------------
+For interactive use of coqtop, we suggest
+- either the Debian cle package
+- or the Proof-General (x)emacs mode, which unfortunately can not be
+distributed by Debian for copyright reasons. However, a Debian package
+might become available at proof general home page in the future
+(http://zermelo.dcs.ed.ac.uk/~proofgen)
+
+However we recommand you to use the CoqIde gtk interface provided in coqide.
+
+
+Unstripped binaries
+-------------------
 
 Note that all bytecode files in this package need to be left
 'unstripped' after compiling. The reason is the following:
@@ -17,12 +40,3 @@ Note that all bytecode files in this package need to be left
 Moreover the bytecode version is installed even on platforms having a
 native version as the dynamic loading of tactics works only with the
 bytecode version.
-
-For interactive use of coqtop, we suggest
-- either the Debian cle package
-- or the Proof-General (x)emacs mode, which unfortunately can not be
-distributed by Debian for copyright reasons. However, a Debian package
-might become available at proof general home page in the future
-(http://zermelo.dcs.ed.ac.uk/~proofgen)
-
-However we recommand you to use the CoqIde gtk interface provided in coqide.