A formalization of geometry in Coq.
This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.
Details and installation instructions can be found here: http://geocoq.github.io/GeoCoq/
Bug reports: https://github.com/GeoCoq/GeoCoq/issues
Mailing list: https://groups.google.com/forum/?hl=fr#!forum/geocoq
