1 files changed, 103 insertions, 0 deletions
diff --git a/debian/control b/debian/control
new file mode 100644
index 00000000..dd90f964
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,103 @@
+Source: coq
+Section: math
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
+Uploaders:
+ Ralf Treinen <treinen@debian.org>,
+ Remi Vanicat <vanicat@debian.org>,
+ Stefano Zacchiroli <zack@debian.org>,
+ Samuel Mimram <smimram@debian.org>,
+ Stephane Glondu <steph@glondu.net>
+DM-Upload-Allowed: yes
+Standards-Version: 3.8.2
+Build-Depends:
+ debhelper (>= 7),
+ dpkg-dev (>= 1.13.19),
+ dh-ocaml (>= 0.4.1),
+ ocaml-nox (>= 3.11.0-5),
+ ocaml-best-compilers,
+ camlp5 (>= 5.12),
+ liblablgtk2-ocaml-dev (>= 2.12.0-3),
+ texlive-latex-extra,
+ hevea (>= 1.10-7)
+Homepage: http://coq.inria.fr/
+Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq.git
+Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq.git
+
+Package: coq
+Architecture: any
+Depends:
+ ${shlibs:Depends},
+ ${misc:Depends},
+ ocaml-base-nox-${F:OCamlABI},
+ coq-theories (= ${source:Version}),
+ emacsen-common
+Provides: coq-${F:CoqABI}
+Recommends: coqide | proofgeneral-coq
+Suggests:
+ ocaml-nox,
+ proofgeneral-coq,
+ ledit | readline-editor,
+ libcoq-ocaml-dev,
+ coq-doc
+Conflicts: coq-libs
+Replaces: coq-libs
+Description: proof assistant for higher-order logic (toplevel and compiler)
+ 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 packages 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-coq
+ package to be installed.
+
+Package: coqide
+Architecture: any
+Depends:
+ ${shlibs:Depends},
+ coq (= ${binary:Version}),
+ ocaml-base-nox-${F:OCamlABI},
+ liblablgtk2-ocaml,
+ ${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.
+
+Package: coq-theories
+Architecture: all
+Depends: coq-${F:CoqABI}, ${misc:Depends}
+Recommends: coq (>= 8.0)
+Conflicts: coq-doc (<= 8.0pl1.0-2), coq-libs
+Replaces: coq-libs
+Description: proof assistant for higher-order logic (theories)
+ 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 existing theories that new proofs can be
+ based upon, including theories of arithmetic and Boolean values.
+
+Package: libcoq-ocaml-dev
+Section: ocaml
+Architecture: any
+Depends:
+ ${shlibs:Depends},
+ coq (= ${binary:Version}),
+ ocaml-nox-${F:OCamlABI},
+ ${misc:Depends}
+Conflicts: coq (<< 8.2-1+dfsg-1), coq-libs
+Replaces: coq (<< 8.2-1+dfsg-1), coq-libs
+Description: development libraries and tools for Coq
+ 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 coqmktop, and libraries needed to develop
+ OCaml-side extensions to Coq.