From 036a8660f11178a2523982d109ba11b99c062a3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 6 Apr 2018 16:30:06 +0200
Subject: Fix #5539: algebraic universe produced by cases.

---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 73be9d6b78..c5a4b4ff0f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1845,7 +1845,7 @@ let build_inversion_problem loc env sigma tms t =
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
   let s' = Retyping.get_sort_of env sigma t in
-  let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
+  let sigma, s = Evd.new_sort_variable univ_flexible sigma in
   let sigma = Evd.set_leq_sort env sigma s' s in
   let evdref = ref sigma in
   let pb =
-- 
cgit v1.2.3