Rewrite sort_universes to minimize the number of universes
Rewrite sort_universes to minimize the number of universes

The whole standard library fits in 3 universes (instead of 22 with the
previous algorithm).

Very costy, time complexity: O(n^4) (if we assume map operations are
done in constant time), with n being the number of universe
variables. It takes ~35s for the whole stdlib.

git-svn-id: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@13796 85f007b7-540e-0410-9357-904b9bb8a0f7

maximedenes/native-coq,maximedenes/native-coq,maximedenes/native-coq