1 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
new file mode 100644
index 00000000..a96a1370
--- /dev/null
+++ b/test-suite/bugs/closed/4390.v
@@ -0,0 +1,37 @@
+Module A.
+Set Printing All.
+Set Printing Universes.
+
+Module M.
+Section foo.
+Universe i.
+End foo.
+End M.
+
+Check Type@{i}.
+(* Succeeds *)
+
+Fail Check Type@{j}.
+(* Error: Undeclared universe: j *)
+
+Definition foo@{j} : Type@{i} := Type@{j}.
+(* ok *)
+End A.
+
+Set Universe Polymorphism.
+Fail Universes j.
+Monomorphic Universe j.
+Section foo.
+  Universes i.
+  Constraint i < j.
+  Definition foo : Type@{j} := Type@{i}.
+  Definition foo' : Type@{j} := Type@{i}.
+End foo.
+
+Check eq_refl : foo@{i} = foo'@{i}.
+
+Definition bar := foo.
+Monomorphic Definition bar'@{k} := foo@{k}.
+
+Fail Constraint j = j.
+Monomorphic Constraint i = i.