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.