Be defensive in univ/eq_instances, raise an anomaly on incompatible instances.
Better hashconsing of levels and universes, working with modules.
Huge slowdown to be tracked in some files, even if no polymorphism is
involved.
- Fix comparison of universes.
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.