HoTT/HoTT — pull request #305 by JasonGross (2014-01-06 05:12:33+00:00)
Title: Pre polyproj fixups

In working on getting HoTT working with the polyproj branch (#301), Matthieu and I made a bunch of changes. In order to see clearly which changes point to bugs in coq, I'm going to merge the improvements that compile with HoTT/coq, and are for well-understood reasons (handling of opacity has changed) or are cosmetic. Since this mostly only touches the category code, and not in any deep way, I'll merge it as soon as I check that it builds correctly.