Merge PR #13299: Remember universe instances of constants in notations

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_6157.v b/test-suite/bugs/closed/bug_6157.v
new file mode 100644
index 0000000000..cd24e4c7ee
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6157.v
@@ -0,0 +1,15 @@
+(* Check that universe instances of refs are preserved *)
+
+Section U.
+Set Universe Polymorphism.
+Definition U@{i} := Type@{i}.
+
+Section foo.
+Universe i.
+Fail Check U@{i} : U@{i}.
+Notation Ui := U@{i}. (* syndef path *)
+Fail Check Ui : Type@{i}.
+Notation "#" := U@{i}. (* non-syndef path *)
+Fail Check # : Type@{i}.
+End foo.
+End U.