summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/changelog6
-rw-r--r--debian/control8
2 files changed, 10 insertions, 4 deletions
diff --git a/debian/changelog b/debian/changelog
index 61876571..bf1a0b67 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+coq (8.0pl2-5) UNRELEASED; urgency=low
+
+ * Removed unnecessary dependency on liblablgtk2-ocaml for coqide.
+
+ -- Samuel Mimram <smimram@debian.org> Wed, 4 Jan 2006 20:15:52 +0100
+
coq (8.0pl2-4) unstable; urgency=low
* Added ocaml309.dpatch patch to compile cleanly with OCaml 3.09,
diff --git a/debian/control b/debian/control
index e6e71135..1474a3f9 100644
--- a/debian/control
+++ b/debian/control
@@ -21,12 +21,12 @@ Description: proof assistant for higher-order logic (toplevel and compiler)
.
A graphical interface for Coq is provided in the coqide package.
Coq can also be used with ProofGeneral, which allows proofs to be
- edited using emacs and xemacs. This requires the proofgeneral-coq
+ edited using emacs and xemacs. This requires the proofgeneral-coq
package to be installed.
Package: coqide
Architecture: any
-Depends: ${shlibs:Depends}, coq (>= 8.0), liblablgtk2-ocaml (>= 2.4.0)
+Depends: ${shlibs:Depends}, coq (>= 8.0)
Description: proof assistant for higher-order logic (gtk interface)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
@@ -60,6 +60,6 @@ Description: proof assistant for higher-order logic (Coq 7 theories)
.
This package provides existing theories from Coq 7 in Coq 8, and
allows proofs that were developed in Coq 7 to be used in Coq 8.
- It is also required to translate theories in Coq 7 syntax into
- the new syntax introduced in Coq 8. However, this package does
+ It is also required to translate theories in Coq 7 syntax into
+ the new syntax introduced in Coq 8. However, this package does
not need to be installed to use Coq 7.