Add doc on the new API for universe polymorphism and primitive projections
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Avoid u+k <= v constraints, don't take the sup of an algebraic universe during
minimization.
Add testsuite for most reported issues on HoTT/coq
Add a tester script
Update test-suite Makefile to handle coq-prog-args