Package: coq Version: 8.3.pl2+dfsg-1~bpo60+1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 18252 Depends: coq-theories (= 8.3.pl2+dfsg-1~bpo60+1), emacsen-common, libcoq-ocaml-pz5k2, ocaml-base-nox-3.11.2, libc6 (>= 2.7) Recommends: coqide | proofgeneral-coq Suggests: ocaml-nox, proofgeneral-coq, ledit | readline-editor, libcoq-ocaml-dev, why (>= 2.19), coq-doc Breaks: coq-libs (<< 8.2.pl1) Replaces: coq-libs (<< 8.2.pl1) Provides: coq-8.3pl2+3.11.2 Homepage: http://coq.inria.fr/ Priority: optional Section: math Filename: pool/main/c/coq/coq_8.3.pl2+dfsg-1~bpo60+1_amd64.deb Size: 5590810 SHA256: 0fc02093d6e782f368a44d2a89df49122d9dcfb367dc81899d238f7eb9f4d2ba SHA1: 88271290fd94f663e70766130f21e754aef33996 MD5sum: 776c3b4d8eaf80f6ab0b1b1d04f3b422 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. . 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: coq-theories Source: coq Version: 8.3.pl2+dfsg-1~bpo60+1 Architecture: all Maintainer: Debian OCaml Maintainers Installed-Size: 138064 Depends: coq-8.3pl2+3.11.2 Recommends: coq (>= 8.0) Breaks: coq-doc (<= 8.0pl1.0-2), coq-libs (<< 8.2.pl1) Replaces: coq-libs (<< 8.2.pl1) Homepage: http://coq.inria.fr/ Priority: optional Section: math Filename: pool/main/c/coq/coq-theories_8.3.pl2+dfsg-1~bpo60+1_all.deb Size: 53100280 SHA256: 0aaadedd17afaee0ce9fb75ad4ec4a7fbbc814dc2f7beb9b5926de5b311223a0 SHA1: abb3c0cb4acfa888f05cdb98e1beeed886ae6308 MD5sum: 3810d570de9d7f823a4c4eb4d28822d7 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: coqide Source: coq Version: 8.3.pl2+dfsg-1~bpo60+1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 18280 Depends: coq (= 8.3.pl2+dfsg-1~bpo60+1), libcoq-ocaml-pz5k2, liblablgtk2-ocaml-h3pg1, ocaml-base-nox-3.11.2, libatk1.0-0 (>= 1.29.3), libc6 (>= 2.7), libcairo2 (>= 1.2.4), libfontconfig1 (>= 2.8.0), libfreetype6 (>= 2.2.1), libglib2.0-0 (>= 2.16.0), libgtk2.0-0 (>= 2.12.0), libpango1.0-0 (>= 1.14.0) Homepage: http://coq.inria.fr/ Priority: optional Section: math Filename: pool/main/c/coq/coqide_8.3.pl2+dfsg-1~bpo60+1_amd64.deb Size: 5534144 SHA256: 136f7d458a5089e0042aea11b7766527e83d8267410ff6c7edf09de670393bb2 SHA1: 1c6229d3bfc1a58e0dd6e14dd3763e2a90a2d69c MD5sum: d70f7ba6bacbe494377d2f9f0cc37f35 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: libcoq-ocaml Source: coq Version: 8.3.pl2+dfsg-1~bpo60+1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 7684 Depends: liblablgtk2-ocaml-h3pg1, ocaml-base-nox-3.11.2, libc6 (>= 2.2.5) Breaks: coq (<< 8.3~), coq-libs, libcoq-ocaml-dev (<< 8.3~) Replaces: coq (<< 8.3~), coq-libs, libcoq-ocaml-dev (<< 8.3~) Provides: libcoq-ocaml-pz5k2 Homepage: http://coq.inria.fr/ Priority: optional Section: ocaml Filename: pool/main/c/coq/libcoq-ocaml_8.3.pl2+dfsg-1~bpo60+1_amd64.deb Size: 2087814 SHA256: f9829e8f251081e8334cb70c23c6f3ff68ddb387a2881e114f2c4a7c2024be12 SHA1: 690f241b3ba134059c5e5be53c3efc90f708c52b MD5sum: a9f6256e9292c028efa21cf273a9d1b6 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 Source: coq Version: 8.3.pl2+dfsg-1~bpo60+1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 25912 Depends: coq (= 8.3.pl2+dfsg-1~bpo60+1), camlp5-jnvc7, libcoq-ocaml-pz5k2, liblablgtk2-ocaml-dev-h3pg1, ocaml-nox-3.11.2, libc6 (>= 2.7) Breaks: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) Replaces: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1) Provides: libcoq-ocaml-dev-pz5k2 Homepage: http://coq.inria.fr/ Priority: optional Section: ocaml Filename: pool/main/c/coq/libcoq-ocaml-dev_8.3.pl2+dfsg-1~bpo60+1_amd64.deb Size: 5889864 SHA256: b89f616c3e640e1a9ff390c28b5e6787093af532ca1675244e38e0ed871476a5 SHA1: 9bc7c2798e2b8468da3703090a5a37184ad99099 MD5sum: b4779687d3e8ae539c0bfa784c0606db 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.