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

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v
new file mode 100644
index 0000000000..48e5568e9b
--- /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.