HoTT/HoTT — pull request #16 by andrejbauer (2012-10-05 20:41:44+00:00)
Title: Major cleanup, usage of custom Coq version

This is a major cleanup of the HoTT library. We depart from Coq 8.3 and 8.4 compatibility for the time being and require a custom version of Coq 8.4 trunk, as explained in INSTALL.txt. The custom version supports the homotopy-theoretic interpretation of identity types, and it allows us to turn universe inconsistencies into warnings. All this is accomplished via command-line options, so the custom version of Coq is in fact compatible with the Coq trunk. We hope to propagate the custom change to the Coq trunk.

The next major change is that the HoTT library comes equipped with its own Coq standard library. At the moment this is a very minimal library, just sufficient to compile HoTT. But we now have the option to really implement a new foundation.

The next major change is configurtion support via autoconf scripts. This makes the library robust, easy to install and to maintain.