blob: cd24e4c7eeec76e0bca9c3326ea076c4a860320e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
|
