Add regression tests for univ. poly. and prim proj

These 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 passes.

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.
Restore implicit arguments of irreflexivity (fixes bug #3305).
Fix second-order matching to properly check that the predicate found by
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq into JasonGross-working-polyproj-tests
Refresh universes for Ltac's type_of, as the term can be used anywhere,
fixing two opened bugs from HoTT/coq.