Parents (Total: 4)

The searched file hash is included in 4 parent files which include package known and seen by metalookup. A sample is included below:

Key	Value
FileSize	3807080
MD5	9A4BC3F1278FB0E2D20E24B0D4624294
PackageDescription	Proof assistant for higher-order logic (Coq 7 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 Camlp4. For more information, see <http://coq.inria.fr/>. . This package provides existing theories from Coq 7 in Coq 8, and allows proofs that were developed in Coq 7 to be used in Coq 8. It is also required to translate theories in Coq 7 syntax into the new syntax introduced in Coq 8. However, this package does not need to be installed to use Coq 7.
PackageMaintainer	Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
PackageName	coq7-libs
PackageSection	math
PackageVersion	8.0pl1-5
SHA-1	05897E67C8EB9688590980DA270E6F3F6C744071
SHA-256	610FCCA9C3FCBB1F39337EC50EFD9913AA4930E5360F126FE299DE8DCBB6A135

Key	Value
FileSize	3728050
MD5	6A1AF93EDFA08F54EA7BAEFBD8E9D680
PackageDescription	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 Camlp4. For more information, see <http://coq.inria.fr/>. . This package provides existing theories that new proofs can be based upon, including theories of arithmetic and Boolean values.
PackageMaintainer	Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
PackageName	coq-libs
PackageSection	math
PackageVersion	8.0pl1-5
SHA-1	3487E1B8786EE4FD5AC32E13F55D8D223DC31B39
SHA-256	CC1585D73DB50C2BA28A3D01B085404FFDCF055A62C724BB5BB835B70F26F739

Key	Value
FileSize	6023652
MD5	9750577602AAA19D1C272A11DEA5152F
PackageDescription	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 Camlp4. For more information, see <http://coq.inria.fr/>. . 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.
PackageMaintainer	Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
PackageName	coq
PackageSection	math
PackageVersion	8.0pl1-5
SHA-1	F776250662FDDBE7CA325FF7FF9AEEBAB13846B1
SHA-256	D9AEE6A7EDF3DEBA975366C7BE8CC8AC210F6BCA73224AD13E1332CB3DD4310D

Key	Value
FileSize	4036702
MD5	8291D2460434DDC1E4D26FEFAF7DDDEE
PackageDescription	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 Camlp4. For more information, see <http://coq.inria.fr/>. . This package provides CoqIde, a graphical user interface for developing proofs.
PackageMaintainer	Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
PackageName	coqide
PackageSection	math
PackageVersion	8.0pl1-5
SHA-1	83BEB2B44D212D39600E71396D27E0B35C3B772A
SHA-256	5636532EF3E88C7DD8B6A84B5DCC8F88750030AE38F1DE32959F9239B20D34A0