From 36f3ae391ee188edb9d858d8832d7fd611db0482 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 21 Feb 2017 12:56:28 +0100
Subject: Univs: fix bug #5365, generation of u+k <= v constraints

Use an explicit label ~algebraic for make_flexible_variable as well.
---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4fd030845..e8380136e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -67,7 +67,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       else t
 	    | UnivFlexible alg ->
 	       if onlyalg && alg then
-	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	         (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
 	       else t))
     | Sort (Prop Pos as s) when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
-- 
cgit v1.2.3