v1.0.4

Replaced Definitions with Theorems and Lemmas and moved the auxiliary functions Forall_tail and Exists_impl to base. These two functions have been added to the latest version of the Coq List library.

v1.0.3

Removed the Relation to Other Work section from the Readme file.

v1.0.2

Revised the Readme file in preparation for submitting the library for inclusion in the Coq Package Index.

v1.0.1

Wrapped the definitions provided by this library within a module to prevent namespace collisions. Also marked the Forall_tail and Exists_impl proofs as local since I plan to eventually ask the library maintainers to add them to the Standard Library.Finally, I renamed pigeons.v to pigeonhole_principle.v for clarity.

v1.0.0

The initial stable release for the Pigeons library. This library provides a stand-alone proof of the Pigeonhole principle.