Use Universe Polymorphism

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

https://coq-community.org/coq-ext-lib/

BSD 2-Clause "Simplified" License

126 stars 46 forks source link

Open gmalecha opened 8 years ago

gmalecha commented 8 years ago

Most things in Structures should be universe polymorphic.

gmalecha commented 4 years ago

There seems to be some new regressions related to changes in Coq, so doing this sooner might be a good idea.