1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
Source: coq
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
Benjamin Barenblat <bbaren@debian.org>,
Ralf Treinen <treinen@debian.org>,
Samuel Mimram <smimram@debian.org>,
Stéphane Glondu <glondu@debian.org>,
Enrico Tassi <gareuselesinge@debian.org>
Standards-Version: 4.3.0
Build-Depends:
debhelper (>= 10),
dh-exec,
dh-ocaml (>= 0.9.5~),
dh-python,
ocaml-nox (>= 4),
ocaml-findlib (>= 1.4),
camlp5 (>= 5.12-2~),
liblablgtk2-ocaml-dev (>= 2.14),
liblablgtksourceview2-ocaml-dev,
libounit-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}),
${ocaml:Depends},
${python3:Depends},
${shlibs:Depends},
${misc:Depends},
ocaml-nox,
ocaml-findlib
Provides: coq-${F:CoqABI}
Suggests:
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.
|
