HoTT/HoTT — pull request #638 by JasonGross (2014-12-12 08:15:35+00:00)
Title: Bump the Coq Submodule and Set Keyed Unification

The long awaited move to the current version of trunk! (Well, current as of two days ago.)

This closes #531 and #557 and #593.

Bumping the submodule gives us some keyed unification, primitive projection, and universe polymorphism fixes. It also gives us a way to debug the unification algorithm used by rewrite. Most visibly (and utterly tangentially), it gives us colored terminal output from, e.g., `Check` and error messages when you run `coqtop` or `coqc` on the command line.

I am mildly concerned about `categories/LaxComma/CoreLaws` which gained 4 seconds (a factor of 2), and `categories/Adjoint/Composition/AssociativityLaw` which gained 5 seconds (a factor of 4), but since these are the worst slowdowns, I'm fine with merging this.

After this, we might finally be able to enable primitive projections in the rest of the library, and also, perhaps, remove `simpl rewrite`.