Rewritten the sorting algorithm for universes with a better complexity.
This should be now linear instead of the cubic Bellman-Ford algorithm.
The new algorithm assumes that the universe graph is a DAG if we remove
the {Le, Eq}-cycles, which is the case when the graph is consistent.
Luckily we only use the sorting algorithm on such consistent graphs,
in the Print Sorted Universes command.
Test-suite for bug #3259.
Fix the behaviour of ML tactic notations w.r.t. Imports by making them
substitutive.
Define [Lift], [lift], and [lower] primitves.
Add a test-case for bug #3314 proving False
Add an extra [Fail] to test-suite/success/univers.v

It's a temporary measure; I left a note to remove the extra [Fail] when
the bug is fixed.