libwhy-coq - Why library for Coq

Property Value
Distribution Debian 7 (Wheezy)
Repository Debian Main i386
Package name libwhy-coq
Package version 2.30+dfsg
Package release 5
Package architecture all
Package type deb
Installed size 903 B
Download size 407.52 KB
Official Mirror
This package contains all useful logical definitions, lemmas with their
proofs and axioms used by Why. Users may need this package when proving
some proof obligations in Coq.


Package Version Architecture Repository
libwhy-coq_2.30+dfsg-5_all.deb 2.30+dfsg all Debian Main
libwhy-coq - - -


Name Value
coq-8.3pl4+3.12.1 -


Name Value
why << 2.18.dfsg-1


Type URL
Binary Package libwhy-coq_2.30+dfsg-5_all.deb
Source Package why

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install libwhy-coq deb package:
    # sudo apt-get install libwhy-coq




2012-05-16 - Mehdi Dogguy <>
why (2.30+dfsg-5) unstable; urgency=low
* Update 0001-Why-2.29-do-support-Coq-8.3.patch
- Mark Coq 8.3pl4 as compatible.
* Bump Standards-Version to 3.9.3, no changes required.
2012-04-06 - St├ęphane Glondu <>
why (2.30+dfsg-4) unstable; urgency=high
* Team upload
* Recompile with coq 8.3pl4 (no changes)
2012-01-16 - Mehdi Dogguy <>
why (2.30+dfsg-3) unstable; urgency=high
* Fix 0002-Mark-alt-ergo-0.93-as-compatible.patch
- Adapt version_regexp because "alt-ergo -version" changed.
* Fix 0004-Default-to-why2-for-jessie-atp.patch
- default to "gui" instead of "why2".
* Add 0007-Replace-caduceus-invocation-by-Frama-C.patch
- Caduceus is gone. We use Frama-C instead.
- Adding Frama-C to Why's dependencies.
* Setting urgency to "high" to fix those issues.
2012-01-12 - Mehdi Dogguy <>
why (2.30+dfsg-2) unstable; urgency=low
* Rebuilt with latest coq-float 1:8.3pl1-1 (no source changes).
2012-01-02 - Mehdi Dogguy <>
why (2.30+dfsg-1) unstable; urgency=low
* New upstream release.
* Update patches:
- Rebase and update existing patches
- add 0004-Default-to-why2-for-jessie-atp.patch
- add 0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
* Add (back) Build-Depends on coq-float.
* Bump build requirement for frama-c to 20111001+nitrogen+dfsg-1~.
* Bump Standards-Version to 3.9.2, no changes needed.
* Fix description-synopsis-starts-with-article in why's description.
* Fix copyright-refers-to-deprecated-bsd-license-file
* Fix spelling-error-in-binary
* Mark Coq 8.3pl3 as compatible with current Why
2011-11-03 - Mehdi Dogguy <>
why (2.29+dfsg-4) unstable; urgency=low
* Rebuild with OCaml 3.12.1.
2011-04-25 - Mehdi Dogguy <>
why (2.29+dfsg-3) unstable; urgency=low
* Remove last added patch. The problem was in Makefile.dynamic, shipped
by frama-c-base which lacks some include statements.
- remove 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
- Bump minimum version number for Frama-C to 20110201+carbon+dfsg-2~.
2011-04-25 - Mehdi Dogguy <>
why (2.29+dfsg-2) unstable; urgency=low
* Fix FTBFS on armel.
- add 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
2011-04-24 - Mehdi Dogguy <>
why (2.29+dfsg-1) unstable; urgency=low
* New upstream release.
- Remove old patches, which are not needed anymore.
- Remove build-depends on coq-float (upstream switched to Flocq which
is not packaged yet).
* Bump minimum version of Coq to 8.3
- and add 0001-Why-2.29-do-support-Coq-8.3.patch (upstream forgot to
mention to why-config that Coq 8.3 is "ok").
* Mark Alt-Ergo 0.93 as compatible
- add 0002-Mark-alt-ergo-0.93-as-compatible.patch
* Fix FTBFS due to non-exhaustive pattern matching
- add 0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
* Set 20110201+carbon+dfsg-1~ as minimum version number for Frama-C.
2011-03-11 - St├ęphane Glondu <>
why (2.26+dfsg-4) unstable; urgency=low
* Team upload
* Rebuild with coq 8.2.pl2+dfsg-2 (no changes)

See Also

Package Description
libwibble-dev_0.1.28-1.1_i386.deb Library of various useful C++ code
libwiki-toolkit-formatter-usemod-perl_0.23-1_all.deb UseModWiki-style formatting for CGI::Wiki
libwiki-toolkit-perl_0.80-1_all.deb Toolkit for building Wikis
libwiki-toolkit-plugin-categoriser-perl_0.08-1_all.deb Category management for Wiki::Toolkit
libwiki-toolkit-plugin-diff-perl_0.12-3_all.deb format differences between two Wiki::Toolkit pages
libwiki-toolkit-plugin-json-perl_0.03-1_all.deb A Wiki::Toolkit plugin to output RecentChanges JSON
libwiki-toolkit-plugin-locator-grid-perl_0.05-4_all.deb A Wiki::Toolkit plugin to manage co-ordinate data
libwiki-toolkit-plugin-ping-perl_0.03-1_all.deb "ping" various services when nodes are written
libwiki-toolkit-plugin-rss-reader-perl_1.6-1_all.deb retrieve RSS feeds for inclusion in Wiki::Toolkit nodes
libwildmidi-config_0.2.3.4-2.1_all.deb software MIDI player configuration
libwildmidi-dev_0.2.3.4-2.1_i386.deb software MIDI player library headers
libwildmidi1_0.2.3.4-2.1_i386.deb software MIDI player library
libwill-paginate-ruby-doc_3.0.3-1_all.deb Transitional package for ruby-will-paginate
libwill-paginate-ruby1.8_3.0.3-1_all.deb Transitional package for ruby-will-paginate
libwill-paginate-ruby_3.0.3-1_all.deb Transitional package for ruby-will-paginate