Implementing the "union by rank" optimisation in the univ.ml

I implemented the "Union by rank" optimization in univ.ml. It is a classical optimization of the union-find algorithm, which is used  in the universes checking algorithm in the kernel of Coq.

I have a file where I get a x15 speed up using this patch, because it helps collapsing long chains of equivalent universes. The standard library gets a reproducible 0.5% speedup.


Regards,
Jacques-Henri Jourdan