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.

---
 pretyping/evarsolve.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96213af9c6..4692fe0057 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       if not onlyalg then refresh_sort status ~direction s
 	       else t
 	    | UnivFlexible alg ->
-	       if onlyalg && alg then
-	         (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
-	       else t))
+               (if alg then
+                  evdref := Evd.make_nonalgebraic_variable !evdref l);
+               t))
       | Set when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
           only refreshing when we want higher universes. *)
-- 
cgit v1.2.3