test-suite/bugs/closed/3825.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Set Universe Polymorphism.
Set Printing Universes.

Axiom foo@{i j} : Type@{i} -> Type@{j}.

Notation bar := foo.

Monomorphic Universes i j.

Check bar@{i j}.
Fail Check bar@{i}.

Notation qux := (nat -> nat).

Fail Check qux@{i}.