Merge PR #7189: Fix #5539: algebraic universe produced by cases.

2 files changed, 16 insertions, 1 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 38196489a..1edce17bd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1850,7 +1850,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 =
diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v
new file mode 100644
index 000000000..48e5568e9
--- /dev/null
+++ b/test-suite/bugs/closed/5539.v
@@ -0,0 +1,15 @@
+Set Universe Polymorphism.
+
+Inductive D : nat -> Type :=
+| DO : D O
+| DS n : D n -> D (S n).
+
+Fixpoint follow (n : nat) : D n -> Prop :=
+  match n with
+  | O => fun d => let 'DO := d in True
+  | S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n')
+  end.
+
+Definition step (n : nat) (d : D n) (H : follow n d) :
+  follow (S n) (DS n d)
+  := H.