From 9bd403ec1b6cedf0542e193774a7af52b27c0a1b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 7 Nov 2018 15:25:59 +0100
Subject: Fix #8908: incorrect refresh of algebraic universes.

---
 engine/uState.mli | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'engine/uState.mli')

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). *)
-- 
cgit v1.2.3