Removing dead code in checker/univ.ml.
Specialize the type of [Univ.compare_neq] so that it is clear it is only used
to recover the trace of a universe inconsistency. Changed its name too btw.
Made explanations for universe inconsistencies optional. They are only used
by the printer anyway.
Compute the trace of a universe inconsistency only when explicitly required
by the printing options (i.e. when "Print Universes" is set).
Fixing Sorting Universes in a world where le and lt constraints may be
redundant in canonical arcs.