HoTT/HoTT — pull request #288 by andrejbauer (2013-12-15 10:20:18+00:00)
Title: Fix @marcbezem's "double entry" 

Let me explain: @marcbezem put in two definitions of the form `Book_X_Y_Z` under a single entry, on the theory that one of them really belonged to a different, still-non-existing entry, and would be moved there eventually. This does not work. If you have two `Book_X_Y_Z` under a single entry they will receive the same number (because the script renumberes all things of the form `Book_X_Y_Z`) and Coq will complain.

You should always run `etc/Book.py` and `make contrib` before making a pull request. That way you will avoid messing things up.

I also put in more instructions on how to add to `contrib/HoTTBook.v`, I'd like some feedback on that. We need better instructions so that kind people, such as @marcbezem, who do the work, don't get confused.