From add9c92bed5d570d3fb4073619d8b4eb84d86848 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 1 Mar 2020 13:32:55 +0100
Subject: test-suite file for spurious universe generation

---
 test-suite/bugs/closed/bug_11722.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11722.v

diff --git a/test-suite/bugs/closed/bug_11722.v b/test-suite/bugs/closed/bug_11722.v
new file mode 100644
index 0000000000..d4bd5f48b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11722.v
@@ -0,0 +1,20 @@
+Require Import Program.
+Set Universe Polymorphism.
+
+Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} :=
+  idpath : paths A a a.
+
+Inductive nat :=
+  | O : nat
+  | S : nat -> nat.
+
+Axiom cheat : forall {A}, A.
+
+Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _.
+Next Obligation.
+  destruct x.
+  constructor.
+  apply cheat.
+Defined. (* FIXED: Universe unbound error *)
+
+Check foo@{_}.
-- 
cgit v1.2.3