coq/coq — pull request #17 by JasonGross (2014-05-06 20:07:05+00:00)
Title: Add more (failing) regression tests for universe polymorphism and primitive projections

hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.

These are the tests that trunk currently fails.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.