aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/prerequisite/bind_univs.v
blob: e834fde11325d3d497603dee0d1a976d9d80a5b2 (plain)
1
2
3
4
5
6
7
(* Used in output/UnivBinders.v *)

Monomorphic Definition mono@{u} := Type@{u}.

Polymorphic Definition poly@{u} := Type@{u}.

Monomorphic Universe reqU.