Adapt coercion code to work with projections as target classes.
HoTT coq bug #82 already fixed.
Fix HoTT bug #84, binding scopes to projections.
Continue fix on argument scopes of primitive projections.
Not considering test-suite file #89 as a bug anymore.
Explicit universes allow to write liftings explicitely. Implicit lifting would change the
theory non-trivially.
Bug closed, now in polymorphic mode, Variables A B : Type give different levels to A and B.
Not a bug, keep for backwards compatibility