Support universe instances on the literal Type

Fixes BZ#5726.

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v
new file mode 100644
index 000000000..53ef47357
--- /dev/null
+++ b/test-suite/bugs/closed/5726.v
@@ -0,0 +1,34 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Module GlobalReference.
+
+  Definition type' := Type.
+  Notation type := type'.
+  Check type@{Set}.
+
+End GlobalReference.
+
+Module TypeLiteral.
+
+  Notation type := Type.
+  Check type@{Set}.
+  Check type@{Prop}.
+
+End TypeLiteral.
+
+Module ExplicitSort.
+  Monomorphic Universe u.
+  Notation foo := Type@{u}.
+  Fail Check foo@{Set}.
+  Fail Check foo@{u}.
+
+  Notation bar := Type.
+  Check bar@{u}.
+End ExplicitSort.
+
+Module PropNotationUnsupported.
+  Notation foo := Prop.
+  Fail Check foo@{Set}.
+  Fail Check foo@{Type}.
+End PropNotationUnsupported.