Univ: try to avoid a few lookup in the universe graph

 Sometimes the same (repr g u) was done in different functions
 after being passed u as argument. We rather try to compute
 (repr g u) as soon as possible, and then pass it instead of u.

 Beware of sync issues : if g changes, arcu might become obsolete
 (cf. setlt, setleq, merge ...)

 Typical code around occurences of declare_univ was doing up to 3
 lookups:
  - is u in g ?
  - if not we descend again in g to add it
  - and then later repr is called on the same u.
 With my safe_repr, we do one lookup if u is in g, and a lookup and
 an addition otherwise. Ok, declare_univ was rarely used, but it seems
 nicer this way.

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

0 files changed, 0 insertions, 0 deletions