HoTT/HoTT — pull request #15 by andrejbauer (2012-09-18 18:02:31+00:00)
Title: Compatibility with Coq 8.4

I have changed the files so that they compile with Coq 8.4. The trouble is that Coq 8.4 has eta conversion, which simplifies a lot of proofs, but breaks the existing code. Also, in 8.4 the hott_simpl tactic is prone to divergence because "autorewrite with paths" diverges. We should find out why.

In the long run it is not clear at all that we want compatibility with Coq 8.4, precisely because of the eta conversion. It is a pain to keep the files working with both 8.3 and 8.4, and I for sure do not intend to do it much longer. I propose that we stop worrying about 8.4 for the time being.