This project contains the Coq sources, the lectures and the exercises for the course
"Programs and Proofs: Mechanizing Mathematics with Dependent Types".
The latest draft of the accompanying lecture notes can be downloaded from the official course page:
Initial release: August 2014
Just run make. This will compile all lecture files, solutions and
create the file latex/pnp.pdf with lecture notes.