coq7-libs 8.0pl3-2 (i386 binary) in ubuntu edgy

 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.