A library for Gradual Certified Programming in Coq
Nicolas Tabareau (Inria) and Éric Tanter (U.Chile)
To compile the coq files, you need the trunk branch of Coq (avalaible at https://github.com/coq, commit c2d053c6).
Simply type 'make' in the repository, coq_makefile will do the rest.