diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_6157.v | 15 |
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. |