coq 8.9.0-1 source package in Ubuntu

Changelog

coq (8.9.0-1) unstable; urgency=high

  * New upstream release
  * Set CAML_LD_LIBRARY_PATH and COQLIB correctly during building
    (Closes: #919462)
  * Coq no longer ships an Emacs mode; users should migrate to Proof
    General (Closes: #736761, #854147, #877938)

 -- Benjamin Barenblat <email address hidden>  Wed, 06 Feb 2019 12:41:09 -0500

Upload details

Uploaded by:
Debian OCaml Maintainers on 2019-02-06
Uploaded to:
Sid
Original maintainer:
Debian OCaml Maintainers
Architectures:
any
Section:
math
Urgency:
Very Urgent

See full publishing history Publishing

Series Pocket Published Component Section
Eoan proposed on 2019-04-18 universe devel

Downloads

File Size SHA-256 Checksum
coq_8.9.0-1.dsc 2.4 KiB a58269491c02821e38e3bcdf27a706679313b566443118320e3e352019f35a0e
coq_8.9.0.orig.tar.gz 5.1 MiB 6468ba1b0e5f0168dcd03b29de573be2198e1a2e0311a99f8d418f4d08458908
coq_8.9.0-1.debian.tar.xz 27.2 KiB a8f122b61740f994bcdb3cc5e96cd82e31ec9e8f3d163b7afe546a590230acbd

Available diffs

No changes file available.

Binary packages built by this source

coq: 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.

coq-dbgsym: debug symbols for coq
coq-theories: 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.

coq-theories-dbgsym: debug symbols for coq-theories
libcoq-ocaml: 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.

libcoq-ocaml-dbgsym: debug symbols for libcoq-ocaml
libcoq-ocaml-dev: 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.