Fix slow Print Universes Subgraph when many ambient universes.

Fix #12688.

Original test:
~~~coq
Record my_mod: Type := mk { datatype: Type; }.
Print Universes Subgraph (my_mod.u0). (* OK *)
From ITree Require Export ITree.      (* using coq-itree for the sake of example *)
Print Universes Subgraph (my_mod.u0). (* Runs forever (> 1 min) *)
~~~

The issue is that we produce a subgraph with the user-given universes
+ Set and Prop. In the test the user given universes are not connected
to other universes, but Set is below every universe so we traverse the
whole graph.

We can go faster by just checking whether Set is strictly below each
universe we're interested in.

Maybe this would be better handled at the ugraph level but that
requires thinking about lbound so I didn't do it.

I tested locally with Require Reals, which makes the print take about
0.1s on my PC before this patch. This is enough to check that we're
now faster (near-instant) but not enough for automatic testing.

Note that the other uses of UGraph.constraints_for (for private
polymorphic universes and for context restriction) are interested in
all ambient universes so the traversals starting at Set end quickly
and do not cause the same issue.

0 files changed, 0 insertions, 0 deletions