summaryrefslogtreecommitdiff
path: root/debian/control
diff options
context:
space:
mode:
Diffstat (limited to 'debian/control')
-rw-r--r--debian/control22
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