Source: coq Section: math Priority: optional Maintainer: Debian OCaml Maintainers Uploaders: Benjamin Barenblat , Ralf Treinen , Samuel Mimram , Stéphane Glondu , Enrico Tassi Standards-Version: 4.3.0 Build-Depends: debhelper (>= 10), dh-exec, dh-ocaml (>= 0.9.5~), dh-python, ocaml-nox (>= 4), ocaml-best-compilers, ocaml-findlib (>= 1.4), camlp5 (>= 5.12-2~), liblablgtk2-ocaml-dev (>= 2.14), liblablgtksourceview2-ocaml-dev, python3, rsync, texlive-latex-extra, hevea (>= 1.10-7) Homepage: http://coq.inria.fr/ Vcs-Browser: https://salsa.debian.org/ocaml-team/coq Vcs-Git: https://salsa.debian.org/ocaml-team/coq.git Package: coq Architecture: any Depends: coq-theories (= ${binary:Version}), emacsen-common, ${ocaml:Depends}, ${python3:Depends}, ${shlibs:Depends}, ${misc:Depends}, ocaml-best-compilers, ocaml-findlib Provides: coq-${F:CoqABI} Suggests: ocaml-nox, proofgeneral, ledit | readline-editor, libcoq-ocaml-dev, why (>= 2.19), coq-doc Breaks: coq-libs (<< 8.2.pl1) Replaces: coq-libs (<< 8.2.pl1) 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 package provides coqtop, a command line interface to Coq. . The proofgeneral package allows proofs to be edited using Emacs and XEmacs. Package: coq-theories Architecture: any Depends: coq-${F:CoqABI}, ${misc:Depends}, ${shlibs:Depends} Recommends: coq (>= 8.0) Breaks: coq-doc (<= 8.0pl1.0-2), coq-libs (<< 8.2.pl1) Replaces: coq-libs (<< 8.2.pl1) 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 Section: ocaml Architecture: any Depends: ${ocaml:Depends}, ${shlibs:Depends}, ${misc:Depends} Provides: ${ocaml:Provides} Breaks: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs Replaces: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs Description: runtime libraries 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 runtime libraries for Coq. Package: libcoq-ocaml-dev Section: ocaml Architecture: any Depends: coq (= ${binary:Version}), ${ocaml:Depends}, ${shlibs:Depends}, ${misc:Depends} Provides: ${ocaml:Provides} Breaks: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) Replaces: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) 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 and libraries needed to develop OCaml-side extensions to Coq.