let_universes.v « success « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/success/let_universes.v

blob: c780ec010f317c227e7e6ebdc529630c03f6219c (plain)

Section S.
Let bla@{} := Prop.
Let bli@{u} := Type@{u}.
Fail Let blo@{} := Type.
End S.