HoTT/HoTT — pull request #261 by JasonGross (2013-11-20 21:03:38+00:00)
Title: Separate categories target

This is on top of #221 and #255, because I don't want to have to go redo those pull requests if this is merged first. The first new commits fix some minor things I forgot in #221 and #255 (that is, including the relevant files in `HoTT.v` and `categories.v`).

This adds separate hott-categories and hott-core targets.

You now need to update `Makefile_targets.mk` if you add a file. I will add this to the wiki after this is merged.

There's now a `strict` target which errors with a useful message if you have `.v` files lying around which aren't included in `Makefile_targets.mk`. There is also the `strict-test` target which does the check, but doesn't build anything. None of these know about ssr.

I'm not sure what the best order of files is in Makefile_targets.mk
(which determines the order in the TOC). In particular, I'm not sure if
we want to enforce a strict "dependencies come first" order, or if we
want a conceptual grouping, and put things in the same folder together.

Currently, we, by default, build both hott-categories and hott-core.
We may decide to change this, and, if we do, we should update travis to
build both. Perhaps we should also add a target for the HoTT book in
contrib?