Fix #8908: incorrect refresh of algebraic universes.

1 files changed, 7 insertions, 1 deletions

diff --git a/engine/uState.mli b/engine/uState.mli
index 8053a7bf83..ad0cd5c1bb 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t
   Turn the variable [l] flexible, and algebraic if [algebraic] is true
   and [l] can be. That is if there are no strict upper constraints on
   [l] and and it does not appear in the instance of any non-algebraic
-  universe. Otherwise the variable is just made flexible. *)
+  universe. Otherwise the variable is just made flexible.
+
+    If [l] is already algebraic it will remain so even with [algebraic:false]. *)
 val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
 
+val make_nonalgebraic_variable : t -> Univ.Level.t -> t
+(** Make the level non algebraic. Undefined behaviour on
+   already-defined algebraics. *)
+
 (** Turn all undefined flexible algebraic variables into simply flexible
    ones. Can be used in case the variables might appear in universe instances
    (typically for polymorphic program obligations). *)