Univ: a faster is_leq test used when possible

 Let's reintroduce the idea of stopping the graph traversal as
 soon as a LE arc has been found, but this time we do so only
 when we're not interested by the LT/LE distinction.

 This way, we should remain correct but avoid largly the time penalty
 induced by the last fix on univ.ml: the +30% on contrib Container
 is almost gone, let's hope it'll be the same with Ssreflect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions