coq/coq — pull request #2 by jhjourdan (2012-11-28 10:53:41+00:00)
Title: 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