bind_univs.v « prerequisite « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/prerequisite/bind_univs.v

blob: f17c00e9d7dc34530cce1a44c4bcefe4dd59b283 (plain)

(* Used in output/UnivBinders.v *)

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

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