Fix #8908: incorrect refresh of algebraic universes.

4 files changed, 16 insertions, 1 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b3848e1b5b..6345046431 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -891,6 +891,9 @@ let make_flexible_variable evd ~algebraic u =
   { evd with universes =
       UState.make_flexible_variable evd.universes ~algebraic u }
 
+let make_nonalgebraic_variable evd u =
+  { evd with universes = UState.make_nonalgebraic_variable evd.universes u }
+
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index be54bebcd7..0a8d1f3287 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -561,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid
 val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map
 (** See [UState.make_flexible_variable] *)
 
+val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
+(** See [UState.make_nonalgebraic_variable]. *)
+
 val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 41905feab7..dc760e7f97 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -577,6 +577,9 @@ let make_flexible_variable ctx ~algebraic u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
+let make_nonalgebraic_variable ctx u =
+  { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic }
+
 let make_flexible_nonalgebraic ctx =
   {ctx with uctx_univ_algebraic = Univ.LSet.empty}
 
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). *)