Mark some progress in the HoTT/coq test-suite

I've marked new failing commands that I'm confused about with "???"; I'm
not sure whether or not they should fail there, but we should keep the
test-suite compiling, probably.
Flattening Level module structure in Univ.
Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq into trunk
Remove unused function in univ
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
Fix module order in printers.mllib
More cleanup/reorganizing of univ.ml to separate constraint/universe handling from
the instance/contexts and substitution code.
Oops, one refactoring was not compiled.
- Fix substitution of universes which needlessly hashconsed existing universes.
- More cleanup. remove unneeded functions in universes
Providing the checker with its own version of the Univ file.
I also took the opportunity to remove a lot of code not used by
the checker.