From fb4978ce2cf0a2d4fc871d5d739eda8618a5184b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 30 Oct 2018 00:10:50 +0100
Subject: Fix #8364: making univ algebraic when already equal to another.

When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.

NB: The bug called make_flexible_variable on Top.15 and
~~~
   {Top.15 Top.14} |= Top.11 < Top.6
                      Top.14 < Top.5
                      Top.11 = Top.15

  ALGEBRAIC UNIVERSES:{Top.17 Top.16}
  UNDEFINED UNIVERSES:Top.17 := Top.14+1
                      Top.16 := Top.14+1
  WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
---
 kernel/uGraph.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index a389b35993..4dbfac5c73 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -73,6 +73,10 @@ val sort_universes : t -> t
    of the universes into equivalence classes. *)
 val constraints_of_universes : t -> Constraint.t * LSet.t list
 
+val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+(** [choose p g u] picks a universe verifying [p] and equal
+   to [u] in [g]. *)
+
 (** [constraints_for ~kept g] returns the constraints about the
    universes [kept] in [g] up to transitivity.
 
-- 
cgit v1.2.3