Stop distributing CoqIDE

CoqIDE currently requires gtksourceview2, which has been removed from
Debian (see https://bugs.debian.org/885677). Upstream has an active
pull request to update to gtksourceview3
(https://github.com/coq/coq/pull/9279), and it looks like Debian may
ship gtksourceview2 with buster anyway, so this is likely to be a
temporary change.

1 files changed, 2 insertions, 20 deletions

diff --git a/debian/control b/debian/control
index 739bb2aa..5af6c74b 100644
--- a/debian/control
+++ b/debian/control
@@ -35,7 +35,6 @@ Depends:
  ocaml-best-compilers,
  ocaml-findlib
 Provides: coq-${F:CoqABI}
-Recommends: coqide | proofgeneral
 Suggests:
  ocaml-nox,
  proofgeneral,
@@ -52,25 +51,8 @@ Description: proof assistant for higher-order logic (toplevel and compiler)
  .
  This package provides coqtop, a command line interface to Coq.
  .
- 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
- package to be installed.
-
-Package: coqide
-Architecture: any
-Depends:
- coq (= ${binary:Version}),
- ${ocaml:Depends},
- ${shlibs:Depends},
- ${misc:Depends}
-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
- specification. It is developed using Objective Caml and Camlp5.
- .
- This package provides CoqIde, a graphical user interface for
- developing proofs.
+ The proofgeneral package allows proofs to be edited using Emacs and
+ XEmacs.
 
 Package: coq-theories
 Architecture: any