HoTT/HoTT — pull request #12 by andrejbauer (2012-06-08 08:33:06+00:00)
Title: Major cleanup of HoTT

This is a major cleanup of the HoTT repository that should not be taken lightly. I tried to keep as much compatibility as possible with existing files, but this was not always possible. A major addition is the hott_simpl tactic which performs a lot of rewriting by itself. I also changed tactics. I put in a large number of comments.

Very likely at the moment some things in HIT and Experimental are broken. But I think on the whole this pull request represents progress. For example, compare proofs in Funext.v as they are in the pull request and as they are in the current version. There is a major cleanup of Mike Shulman's equivalences proofs. In many cases the proofs are not as monolithic and are equipped with comments on what is going on.

I would like someone who is not me to review the changes and make the pull, if they think it is acceptable.